Theorem sbel2x
Elimination of double substitution. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
(New usage is discouraged.)
Conclusion
\( \vdash \varphi \leftrightarrow \exists x \, \exists y \, (x = z \wedge y = w \wedge [ y / w ] \, [ x / z ] \, \varphi) \)
Proof
l0
nfv
nfv
l2
2sb5rf l0 _
\( \vdash \varphi \leftrightarrow \exists y \, \exists x \, (y = w \wedge x = z \wedge [ y / w ] \, [ x / z ] \, \varphi) \)
ancom
anbi1i _
l5
2exbii _
\( \vdash \exists y \, \exists x \, (y = w \wedge x = z \wedge [ y / w ] \, [ x / z ] \, \varphi) \leftrightarrow \exists y \, \exists x \, (x = z \wedge y = w \wedge [ y / w ] \, [ x / z ] \, \varphi) \)
excom
\( \vdash \exists y \, \exists x \, (x = z \wedge y = w \wedge [ y / w ] \, [ x / z ] \, \varphi) \leftrightarrow \exists x \, \exists y \, (x = z \wedge y = w \wedge [ y / w ] \, [ x / z ] \, \varphi) \)
3bitri l2 l5 _