Metamath Proof Explorer


Theorem axextdist

Description: ax-ext with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010)

Ref Expression
Assertion axextdist ¬ z z = x ¬ z z = y z z x z y x = y

Proof

Step Hyp Ref Expression
1 nfnae z ¬ z z = x
2 nfnae z ¬ z z = y
3 1 2 nfan z ¬ z z = x ¬ z z = y
4 nfcvf ¬ z z = x _ z x
5 4 adantr ¬ z z = x ¬ z z = y _ z x
6 5 nfcrd ¬ z z = x ¬ z z = y z w x
7 nfcvf ¬ z z = y _ z y
8 7 adantl ¬ z z = x ¬ z z = y _ z y
9 8 nfcrd ¬ z z = x ¬ z z = y z w y
10 6 9 nfbid ¬ z z = x ¬ z z = y z w x w y
11 elequ1 w = z w x z x
12 elequ1 w = z w y z y
13 11 12 bibi12d w = z w x w y z x z y
14 13 a1i ¬ z z = x ¬ z z = y w = z w x w y z x z y
15 3 10 14 cbvald ¬ z z = x ¬ z z = y w w x w y z z x z y
16 axextg w w x w y x = y
17 15 16 syl6bir ¬ z z = x ¬ z z = y z z x z y x = y