Metamath Proof Explorer

Theorem ax5el

Description: Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-5 considered as a metatheorem.) (Contributed by NM, 22-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax5el x y z x y


Step Hyp Ref Expression
1 ax-c14 ¬ z z = x ¬ z z = y x y z x y
2 ax-c16 z z = x x y z x y
3 ax-c16 z z = y x y z x y
4 1 2 3 pm2.61ii x y z x y