Theorem sb7f
This version of dfsb7 does not require that \( \varphi \) and \( z \) be
disjoint. This permits it to be used as a definition for substitution
in a formalization that omits the logically redundant axiom [ax-5],
i.e., that does not have the concept of a variable not occurring in a
formula. (Definition dfsb1 is also suitable, but its mixing of free
and bound variables is distasteful to some logicians.) Usage of this
theorem is discouraged because it depends on [ax-13]. (Contributed by
NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.)
(New usage is discouraged.)
Hypothesis
sb7f.1
\( \vdash \Finv z \, \varphi \)
Conclusion
\( \vdash [ y' / x ] \, \varphi \leftrightarrow \exists z \, (z = y' \wedge \exists x \, (x = z \wedge \varphi)) \)
Proof
sb7f.1
sb5f _
l2
sbbii _
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / z ] \, \exists x \, (x = z \wedge \varphi) \)
sb7f.1
l4
sbco2 _
\( \vdash [ y' / z ] \, [ z / x ] \, \varphi \leftrightarrow [ y' / x ] \, \varphi \)
sb5
\( \vdash [ y' / z ] \, \exists x \, (x = z \wedge \varphi) \leftrightarrow \exists z \, (z = y' \wedge \exists x \, (x = z \wedge \varphi)) \)
3bitr3i l2 l4 _