Theorem cbveuw
Version of cbveu with a disjoint variable condition, which does not
require [ax-10], [ax-13]. (Contributed by NM, 25-Nov-1994.) (Revised
by GG, 23-May-2024.)
Hypotheses
cbveuw.1
\( \vdash \Finv y \, \varphi \)
cbveuw.2
\( \vdash \Finv x \, \psi \)
cbveuw.3
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, \psi \)
Proof
l0
cbveuw.1
l1
cbveuw.2
cbveuw.3
l3
cbvexv1 l0 l1 _
l4
cbveuw.1
l5
cbveuw.2
cbveuw.3
cbvmow 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 _