Theorem sb8eulem
Lemma. Factor out the common proof skeleton of sb8euv and sb8eu.
Variable substitution in unique existential quantifier. (Contributed by
NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof
shortened by Wolf Lammen, 24-Aug-2019.) Factor out common proof lines.
(Revised by Wolf Lammen, 9-Feb-2023.)
Hypothesis
sb8eulem.nfsb
\( \vdash \Finv y \, [ w / x ] \, \varphi \)
Conclusion
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists{!} y \, [ y / x ] \, \varphi \)
Proof
l0
sb8v
\( \vdash \forall x \, (\varphi \leftrightarrow x = z) \leftrightarrow \forall w \, [ w / x ] \, (\varphi \leftrightarrow x = z) \)
equsb3
sblbis _
l3
albii _
\( \vdash \forall w \, [ w / x ] \, (\varphi \leftrightarrow x = z) \leftrightarrow \forall w \, ([ w / x ] \, \varphi \leftrightarrow w = z) \)
l4
sb8eulem.nfsb
nfv
l6
nfbi l4 _
l7
nfv
l8
sbequ
equequ1
bibi12d l8 _
cbvalv1 l6 l7 _
\( \vdash \forall w \, ([ w / x ] \, \varphi \leftrightarrow w = z) \leftrightarrow \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = z) \)
3bitri l0 l3 _
l13
exbii _
\( \vdash \exists z \, \forall x \, (\varphi \leftrightarrow x = z) \leftrightarrow \exists z \, \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = z) \)
l14
eu6
\( \vdash \exists{!} x \, \varphi \leftrightarrow \exists z \, \forall x \, (\varphi \leftrightarrow x = z) \)
eu6
\( \vdash \exists{!} y \, [ y / x ] \, \varphi \leftrightarrow \exists z \, \forall y \, ([ y / x ] \, \varphi \leftrightarrow y = z) \)
3bitr4i l13 l14 _