Theorem n0elqs

Description: Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019)

	Ref	Expression
Assertion	n0elqs	⊢ ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ 𝐴 ⊆ dom 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	⊢ ( 𝑥 ∈ dom 𝑅 ↔ [ 𝑥 ] 𝑅 ≠ ∅ )
2	1	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ≠ ∅ )
3		dfss3	⊢ ( 𝐴 ⊆ dom 𝑅 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom 𝑅 )
4		nne	⊢ ( ¬ [ 𝑥 ] 𝑅 ≠ ∅ ↔ [ 𝑥 ] 𝑅 = ∅ )
5	4	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ [ 𝑥 ] 𝑅 ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∅ )
6	5	notbii	⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ¬ [ 𝑥 ] 𝑅 ≠ ∅ ↔ ¬ ∃ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∅ )
7		dfral2	⊢ ( ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ≠ ∅ ↔ ¬ ∃ 𝑥 ∈ 𝐴 ¬ [ 𝑥 ] 𝑅 ≠ ∅ )
8		0ex	⊢ ∅ ∈ V
9	8	elqs	⊢ ( ∅ ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 ∅ = [ 𝑥 ] 𝑅 )
10		eqcom	⊢ ( ∅ = [ 𝑥 ] 𝑅 ↔ [ 𝑥 ] 𝑅 = ∅ )
11	10	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∅ = [ 𝑥 ] 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∅ )
12	9 11	bitri	⊢ ( ∅ ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∅ )
13	12	notbii	⊢ ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∅ )
14	6 7 13	3bitr4ri	⊢ ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ≠ ∅ )
15	2 3 14	3bitr4ri	⊢ ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ 𝐴 ⊆ dom 𝑅 )