This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 )