Metamath Proof Explorer

Theorem elqsn0

Description: A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion elqsn0 
|- ( ( dom R = A /\ B e. ( A /. R ) ) -> B =/= (/) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( A /. R ) = ( A /. R )
2 neeq1 
 |-  ( [ x ] R = B -> ( [ x ] R =/= (/) <-> B =/= (/) ) )
3 eleq2 
 |-  ( dom R = A -> ( x e. dom R <-> x e. A ) )
4 3 biimpar 
 |-  ( ( dom R = A /\ x e. A ) -> x e. dom R )
5 ecdmn0 
 |-  ( x e. dom R <-> [ x ] R =/= (/) )
6 4 5 sylib 
 |-  ( ( dom R = A /\ x e. A ) -> [ x ] R =/= (/) )
7 1 2 6 ectocld 
 |-  ( ( dom R = A /\ B e. ( A /. R ) ) -> B =/= (/) )