Theorem equsalh

An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on [ax-13]. See equsalhw for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)

Hypotheses

equsalh.1

\( \vdash \psi \rightarrow \forall x \, \psi \)

equsalh.2

\( \vdash x = y' \rightarrow (\varphi \leftrightarrow \psi) \)

Conclusion

\( \vdash \forall x \, (x = y' \rightarrow \varphi) \leftrightarrow \psi \)

Proof

equsalh.1

nf5i _

equsalh.2

equsal l1 _