Theorem mo4
At-most-one quantifier expressed using implicit substitution. This
theorem is also a direct consequence of mo4f, but this proof is based
on fewer axioms.
Note: Swapping both \( x \), \( y \) and \( \varphi \), \( \psi \) preserves the
hypothesis and DV conditions, so we also have the conclusion
\( \vdash \exists^\ast y \, \psi \leftrightarrow \forall y \, \forall x \, (\psi \wedge \varphi \rightarrow y = x) \). But under
the hypothesis and DV condition, we also have
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, \psi \) (that is a proof step). Therefore, since
\( \vdash \varphi \wedge \psi \leftrightarrow (\psi \leftrightarrow \varphi) \) ( ancom) and
\( \vdash x = y \leftrightarrow y = x \) ( equcom) , we obtain, still under the
hypothesis and DV condition,
|- ( A. x A. y ( ( ph /\ ps ) -> x = y ) <->
A. y A. x ( ( ph /\ ps ) -> x = y ) ); in other words, in this
special case we can swap universal quantifiers as in alcom without
requiring [ax-11]. (Contributed by NM, 26-Jul-1995.) Reduce axiom
usage. (Revised by Wolf Lammen, 18-Oct-2023.)
Hypothesis
mo4.1
\( \vdash x = y \rightarrow (\varphi \leftrightarrow \psi) \)
Conclusion
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
Proof
l0
dfmo
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
l1
mo4.1
equequ1
imbi12d l1 _
l4
cbvalvw _
l5
biimpi _
\( \vdash \forall x \, (\varphi \rightarrow x = z) \rightarrow \forall y \, (\psi \rightarrow y = z) \)
l6
pm2.27
pm2.27
l8
im2anan9 l6 _
\( \vdash \varphi \wedge \psi \rightarrow (\varphi \rightarrow x = z) \wedge (\psi \rightarrow y = z) \rightarrow x = z \wedge y = z \)
equtr2
\( \vdash x = z \wedge y = z \rightarrow x = y \)
syl6com l8 _
ex _
alimdv _
com12 _
alimdv _
\( \vdash \forall y \, (\psi \rightarrow y = z) \rightarrow \forall x \, (\varphi \rightarrow x = z) \rightarrow \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
mpcom l5 _
exlimiv _
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \rightarrow \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \)
l17
sylbi l0 _
mo4.1
cbvexvw _
l20
biimpri _
\( \vdash \exists y \, \psi \rightarrow \exists x \, \varphi \)
l21
ax6evr
\( \vdash \exists z \, x = z \)
pm3.2
l23
imim1d _
\( \vdash \varphi \rightarrow (\varphi \wedge \psi \rightarrow x = y) \rightarrow \psi \rightarrow x = y \)
ax7
\( \vdash x = y \rightarrow x = z \rightarrow y = z \)
syl8 l23 _
com4r _
impcom _
alimdv _
impancom _
eximdv _
\( \vdash \varphi \wedge \forall y \, (\varphi \wedge \psi \rightarrow x = y) \rightarrow \exists z \, x = z \rightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l31
mpi l21 _
\( \vdash \varphi \wedge \forall y \, (\varphi \wedge \psi \rightarrow x = y) \rightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l32
dfmo
\( \vdash \exists^\ast y \, \psi \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
sylibr l31 _
expcom _
l35
aleximi _
\( \vdash \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \rightarrow \exists x \, \varphi \rightarrow \exists x \, \exists^\ast y \, \psi \)
ax5e
\( \vdash \exists x \, \exists^\ast y \, \psi \rightarrow \exists^\ast y \, \psi \)
l37
syl56 l20 l35 _
\( \vdash \forall x \, \forall y \, (\varphi \wedge \psi \rightarrow x = y) \rightarrow \exists y \, \psi \rightarrow \exists^\ast y \, \psi \)
exbii l4
\( \vdash \exists z \, \forall x \, (\varphi \rightarrow x = z) \leftrightarrow \exists z \, \forall y \, (\psi \rightarrow y = z) \)
l39
3bitr4i _ l0 l32
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists^\ast y \, \psi \)
moabs
\( \vdash \exists^\ast y \, \psi \leftrightarrow \exists y \, \psi \rightarrow \exists^\ast y \, \psi \)
bitri l39 _
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists y \, \psi \rightarrow \exists^\ast y \, \psi \)
sylibr l37 _
impbii l17 _