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