Theorem n0elim

Description: Implication of that the empty set is not an element of a class. (Contributed by Peter Mazsa, 30-Dec-2024)

	Ref	Expression
Assertion	n0elim	⊢ ( ¬ ∅ ∈ 𝐴 → ( 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 ↾ 𝐴 ) ) = 𝐴 )