Theorem distel

Description: Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el and elirrv .) (Contributed by Scott Fenton, 15-Dec-2010)

	Ref	Expression
Assertion	distel	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ↔ ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		el	⊢ ∃ 𝑧 𝑥 ∈ 𝑧
2		df-ex	⊢ ( ∃ 𝑧 𝑥 ∈ 𝑧 ↔ ¬ ∀ 𝑧 ¬ 𝑥 ∈ 𝑧 )
3		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑥
4		dveel1	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( 𝑥 ∈ 𝑧 → ∀ 𝑦 𝑥 ∈ 𝑧 ) )
5	3 4	nf5d	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 ∈ 𝑧 )
6	5	nfnd	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 ¬ 𝑥 ∈ 𝑧 )
7		elequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝑦 ) )
8	7	notbid	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑦 ) )
9	8	a1i	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( 𝑧 = 𝑦 → ( ¬ 𝑥 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑦 ) ) )
10	3 6 9	cbvald	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∀ 𝑧 ¬ 𝑥 ∈ 𝑧 ↔ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ) )
11	10	notbid	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ¬ ∀ 𝑧 ¬ 𝑥 ∈ 𝑧 ↔ ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ) )
12	2 11	bitrid	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑧 𝑥 ∈ 𝑧 ↔ ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 ) )
13	1 12	mpbii	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 )
14		elirrv	⊢ ¬ 𝑦 ∈ 𝑦
15		elequ1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
16	14 15	mtbii	⊢ ( 𝑦 = 𝑥 → ¬ 𝑥 ∈ 𝑦 )
17	16	alimi	⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 )
18	17	con3i	⊢ ( ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 → ¬ ∀ 𝑦 𝑦 = 𝑥 )
19	13 18	impbii	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 ↔ ¬ ∀ 𝑦 ¬ 𝑥 ∈ 𝑦 )