Theorem cbveuALT
Alternative proof of cbveu. Since [df-eu] combines two other
quantifiers, one can base this theorem on their associated 'change
bounded variable' kind of theorems as well. (Contributed by Wolf
Lammen, 5-Jan-2023.) (Proof modification is discouraged.)
(New usage is discouraged.)
Hypotheses
cbveu.1
\( \vdash \Finv y \, \varphi \)
cbveu.2
\( \vdash \Finv x \, \psi \)
cbveu.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, \psi \)
Proof
l0
cbveu.1
l1
cbveu.2
cbveu.3
l3
cbvex l0 l1 _
l4
cbveu.1
l5
cbveu.2
cbveu.3
cbvmo l4 l5 _
l8
anbi12i l3 _
\( \vdash \exists x \, \varphi \wedge \exists^\ast x \, \varphi \leftrightarrow \exists y \, \psi \wedge \exists^\ast y \, \psi \)
l9
df-eu
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists x \, \varphi \wedge \exists^\ast x \, \varphi \)
df-eu
\( \vdash \exists{!} y \, \psi \leftrightarrow \exists y \, \psi \wedge \exists^\ast y \, \psi \)
3bitr4i l8 l9 _