Theorem axextbdist

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

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

Proof

Step	Hyp	Ref	Expression
1		axc9	⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) ) )
2	1	imp	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 = 𝑦 → ∀ 𝑧 𝑥 = 𝑦 ) )
3		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑥
4		nfnae	⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑦
5	3 4	nfan	⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 )
6		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
7	6	a1i	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
8	5 7	alimd	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑧 𝑥 = 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
9	2 8	syld	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 = 𝑦 → ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )
10		axextdist	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) )
11	9 10	impbid	⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ) → ( 𝑥 = 𝑦 ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) ) )