Theorem sb10f

Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. Usage of this theorem is discouraged because it depends on [ax-13]. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)

Hypothesis
sb10f.1
\( \vdash \Finv x \, \varphi \)
Conclusion
\( \vdash [ y' / z ] \, \varphi \leftrightarrow \exists x \, (x = y' \wedge [ x / z ] \, \varphi) \)
Proof
sb10f.1
l1
nfsb _
sbequ
equsexv l1 _
bicomi _