Theorem 2sb6rf
Reversed double substitution. Usage of this theorem is discouraged
because it depends on [ax-13]. (Contributed by NM, 3-Feb-2005.)
(Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints.
(Revised by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen,
13-Apr-2023.) (New usage is discouraged.)
Hypotheses
2sb5rf.1
\( \vdash \Finv z \, \varphi \)
2sb5rf.2
\( \vdash \Finv w \, \varphi \)
Conclusion
\( \vdash \varphi \leftrightarrow \forall z \, \forall w \, (z = x \wedge w = y \rightarrow [ z / x ] \, [ w / y ] \, \varphi) \)
Proof
2sb5rf.1
l1
19.23 _
\( \vdash \forall z \, (\exists w \, (z = x \wedge w = y) \rightarrow \varphi) \leftrightarrow \exists z \, \exists w \, (z = x \wedge w = y) \rightarrow \varphi \)
2sb5rf.2
19.23 _
l4
albii _
\( \vdash \forall z \, \forall w \, (z = x \wedge w = y \rightarrow \varphi) \leftrightarrow \forall z \, (\exists w \, (z = x \wedge w = y) \rightarrow \varphi) \)
2ax6e
a1bi _
\( \vdash \varphi \leftrightarrow \exists z \, \exists w \, (z = x \wedge w = y) \rightarrow \varphi \)
l7
3bitr4ri l1 l4 _
\( \vdash \varphi \leftrightarrow \forall z \, \forall w \, (z = x \wedge w = y \rightarrow \varphi) \)
l8
sbequ12r
\( \vdash z = x \rightarrow ([ z / x ] \, [ w / y ] \, \varphi \leftrightarrow [ w / y ] \, \varphi) \)
sbequ12r
\( \vdash w = y \rightarrow ([ w / y ] \, \varphi \leftrightarrow \varphi) \)
sylan9bb l8 _
pm5.74i _
2albii _
\( \vdash \forall z \, \forall w \, (z = x \wedge w = y \rightarrow [ z / x ] \, [ w / y ] \, \varphi) \leftrightarrow \forall z \, \forall w \, (z = x \wedge w = y \rightarrow \varphi) \)
bitr4i l7 _