Metamath Proof Explorer

Theorem n0eldmqs

Description: The empty set is not an element of a domain quotient. (Contributed by Peter Mazsa, 2-Mar-2018)

Ref Expression
Assertion n0eldmqs 
|- -. (/) e. ( dom R /. R )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  dom R C_ dom R
2 n0elqs 
 |-  ( -. (/) e. ( dom R /. R ) <-> dom R C_ dom R )
3 1 2 mpbir 
 |-  -. (/) e. ( dom R /. R )