Theorem 2mos
Double "there exists at most one", using implicit substitution.
(Contributed by NM, 10-Feb-2005.) (Proof shortened by Wolf Lammen,
21-May-2025.)
Hypothesis
2mos.1
\( \vdash x = z \wedge y = w \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge \psi \rightarrow x = z \wedge y = w) \)
Proof
l0
2mo
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \)
2mos.1
2sbievw _
anbi2i _
imbi1i _
2albii _
2albii _
\( \vdash \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge [ z / x ] \, [ w / y ] \, \varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, \forall z \, \forall w \, (\varphi \wedge \psi \rightarrow x = z \wedge y = w) \)
bitri l0 _