Description: Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of Suppes p. 89. (Contributed by NM, 10-Dec-2003)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | map0.1 | |- A e. _V |
|
| map0.2 | |- B e. _V |
||
| Assertion | map0 | |- ( ( A ^m B ) = (/) <-> ( A = (/) /\ B =/= (/) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | map0.1 | |- A e. _V |
|
| 2 | map0.2 | |- B e. _V |
|
| 3 | map0g | |- ( ( A e. _V /\ B e. _V ) -> ( ( A ^m B ) = (/) <-> ( A = (/) /\ B =/= (/) ) ) ) |
|
| 4 | 1 2 3 | mp2an | |- ( ( A ^m B ) = (/) <-> ( A = (/) /\ B =/= (/) ) ) |