Theorem eu6lem
Lemma of eu6im. A dissection of an idiom characterizing existential
uniqueness. (Contributed by NM, 12-Aug-1993.) This used to be the
definition of the unique existential quantifier, while [df-eu] was then
proved as dfeu. (Revised by BJ, 30-Sep-2022.) (Proof shortened by
Wolf Lammen, 3-Jan-2023.) Extract common proof lines. (Revised by Wolf
Lammen, 3-Mar-2023.)
Conclusion
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
Proof
l0
19.42v
\( \vdash \exists z \, (\forall x \, (\varphi \leftrightarrow x = y) \wedge y = z) \leftrightarrow \forall x \, (\varphi \leftrightarrow x = y) \wedge \exists z \, y = z \)
l1
alsyl
\( \vdash \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z) \rightarrow \forall x \, (x = y \rightarrow x = z) \)
equvelv
\( \vdash \forall x \, (x = y \rightarrow x = z) \leftrightarrow y = z \)
sylib l1 _
l4
pm4.71i _
\( \vdash \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z) \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z) \wedge y = z \)
albiim
l6
biancomi _
\( \vdash \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = y) \)
equequ2
imbi2d _
albidv _
anbi2d _
\( \vdash y = z \rightarrow (\forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = y) \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z)) \)
bitrid l6 _
pm5.32ri _
\( \vdash \forall x \, (\varphi \leftrightarrow x = y) \wedge y = z \leftrightarrow \forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z) \wedge y = z \)
bitr4i l4 _
l14
exbii _
\( \vdash \exists z \, (\forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z)) \leftrightarrow \exists z \, (\forall x \, (\varphi \leftrightarrow x = y) \wedge y = z) \)
ax6evr
biantru _
\( \vdash \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \forall x \, (\varphi \leftrightarrow x = y) \wedge \exists z \, y = z \)
3bitr4ri l0 l14 _
l18
exbii _
\( \vdash \exists y \, \forall x \, (\varphi \leftrightarrow x = y) \leftrightarrow \exists y \, \exists z \, (\forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z)) \)
exdistrv
\( \vdash \exists y \, \exists z \, (\forall x \, (x = y \rightarrow \varphi) \wedge \forall x \, (\varphi \rightarrow x = z)) \leftrightarrow \exists y \, \forall x \, (x = y \rightarrow \varphi) \wedge \exists z \, \forall x \, (\varphi \rightarrow x = z) \)
bitri l18 _