Theorem axextdist

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

	Ref	Expression
Assertion	axextdist	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑥
2		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑦
3	1 2	nfan	⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 )
4		nfcvf	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 )
5	4	adantr	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑥 )
6	5	nfcrd	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑤 ∈ 𝑥 )
7		nfcvf	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑦 )
8	7	adantl	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑦 )
9	8	nfcrd	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 𝑤 ∈ 𝑦 )
10	6 9	nfbid	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → Ⅎ 𝑧 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) )
11		elequ1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
12		elequ1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
13	11 12	bibi12d	⊢ ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
14	13	a1i	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑤 = 𝑧 → ( ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) ) )
15	3 10 14	cbvald	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
16		axextg	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) → 𝑥 = 𝑦 )
17	15 16	syl6bir	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )