Theorem n0el2

Description: Two ways of expressing that the empty set is not an element of a class. (Contributed by Peter Mazsa, 31-Jan-2018)

	Ref	Expression
Assertion	n0el2	⊢ ( ¬ ∅ ∈ 𝐴 ↔ dom ( ◡ E ↾ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dmopab3	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ 𝑥 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } = 𝐴 )
2		n0el	⊢ ( ¬ ∅ ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ 𝑥 )
3		cnvepres	⊢ ( ◡ E ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
4	3	dmeqi	⊢ dom ( ◡ E ↾ 𝐴 ) = dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) }
5	4	eqeq1i	⊢ ( dom ( ◡ E ↾ 𝐴 ) = 𝐴 ↔ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥 ) } = 𝐴 )
6	1 2 5	3bitr4i	⊢ ( ¬ ∅ ∈ 𝐴 ↔ dom ( ◡ E ↾ 𝐴 ) = 𝐴 )