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 
|- ( -. (/) e. ( A /. R ) <-> dom ( R |` A ) = A )

Proof

Step Hyp Ref Expression
1 n0elqs 
 |-  ( -. (/) e. ( A /. R ) <-> A C_ dom R )
2 ssdmres 
 |-  ( A C_ dom R <-> dom ( R |` A ) = A )
3 1 2 bitri 
 |-  ( -. (/) e. ( A /. R ) <-> dom ( R |` A ) = A )