Metamath Proof Explorer


Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6vsep ¬ x ¬ x = y

Proof

Step Hyp Ref Expression
1 ax-sep x z z x z y z = z z = z
2 id z = z z = z
3 2 biantru z y z y z = z z = z
4 3 bibi2i z x z y z x z y z = z z = z
5 4 biimpri z x z y z = z z = z z x z y
6 5 alimi z z x z y z = z z = z z z x z y
7 ax-ext z z x z y x = y
8 6 7 syl z z x z y z = z z = z x = y
9 8 eximi x z z x z y z = z z = z x x = y
10 1 9 ax-mp x x = y
11 df-ex x x = y ¬ x ¬ x = y
12 10 11 mpbi ¬ x ¬ x = y