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