Theorem elqsn0

Description: A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995)

	Ref	Expression
Assertion	elqsn0	⊢ ( ( dom 𝑅 = 𝐴 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 / 𝑅 ) = ( 𝐴 / 𝑅 )
2		neeq1	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 ≠ ∅ ↔ 𝐵 ≠ ∅ ) )
3		eleq2	⊢ ( dom 𝑅 = 𝐴 → ( 𝑥 ∈ dom 𝑅 ↔ 𝑥 ∈ 𝐴 ) )
4	3	biimpar	⊢ ( ( dom 𝑅 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅 )
5		ecdmn0	⊢ ( 𝑥 ∈ dom 𝑅 ↔ [ 𝑥 ] 𝑅 ≠ ∅ )
6	4 5	sylib	⊢ ( ( dom 𝑅 = 𝐴 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑥 ] 𝑅 ≠ ∅ )
7	1 2 6	ectocld	⊢ ( ( dom 𝑅 = 𝐴 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ≠ ∅ )