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 =/= (/) )