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 ¬ A / R dom R A = A

Proof

Step Hyp Ref Expression
1 n0elqs ¬ A / R A dom R
2 ssdmres A dom R dom R A = A
3 1 2 bitri ¬ A / R dom R A = A