Metamath Proof Explorer


Theorem n0elqs2

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

Ref Expression
Assertion n0elqs2 ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ dom ( 𝑅𝐴 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 n0elqs ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ 𝐴 ⊆ dom 𝑅 )
2 ssdmres ( 𝐴 ⊆ dom 𝑅 ↔ dom ( 𝑅𝐴 ) = 𝐴 )
3 1 2 bitri ( ¬ ∅ ∈ ( 𝐴 / 𝑅 ) ↔ dom ( 𝑅𝐴 ) = 𝐴 )