Metamath Proof Explorer

Theorem n0eldmqseq

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

Ref Expression
Assertion n0eldmqseq 
|- ( ( dom R /. R ) = A -> -. (/) e. A )

Proof

Step Hyp Ref Expression
1 n0eldmqs 
 |-  -. (/) e. ( dom R /. R )
2 eleq2 
 |-  ( ( dom R /. R ) = A -> ( (/) e. ( dom R /. R ) <-> (/) e. A ) )
3 1 2 mtbii 
 |-  ( ( dom R /. R ) = A -> -. (/) e. A )