Metamath Proof Explorer

Theorem ax12f

Description: Basis step for constructing a substitution instance of ax-c15 without using ax-c15 . We can start with any formula ph in which x is not free. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12f.1 φ x φ
Assertion ax12f ¬ x x = y x = y φ x x = y φ


Step Hyp Ref Expression
1 ax12f.1 φ x φ
2 ax-1 φ x = y φ
3 1 2 alrimih φ x x = y φ
4 3 2a1i ¬ x x = y x = y φ x x = y φ