Theorem n0el3

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

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

Proof

Step	Hyp	Ref	Expression
1		n0el2	⊢ ( ¬ ∅ ∈ 𝐴 ↔ dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
2	1	biimpi	⊢ ( ¬ ∅ ∈ 𝐴 → dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
3	2	qseq1d	⊢ ( ¬ ∅ ∈ 𝐴 → ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = ( 𝐴 / ( ◡ E ↾ 𝐴 ) ) )
4		qsresid	⊢ ( 𝐴 / ( ◡ E ↾ 𝐴 ) ) = ( 𝐴 / ◡ E )
5		qsid	⊢ ( 𝐴 / ◡ E ) = 𝐴
6	4 5	eqtri	⊢ ( 𝐴 / ( ◡ E ↾ 𝐴 ) ) = 𝐴
7	3 6	eqtrdi	⊢ ( ¬ ∅ ∈ 𝐴 → ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
8		n0eldmqseq	⊢ ( ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 → ¬ ∅ ∈ 𝐴 )
9	7 8	impbii	⊢ ( ¬ ∅ ∈ 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 )