This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union The mapping operation map0
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 ∈ V
map0.2 ⊢ B ∈ V
Assertion
map0 ⊢ A B = ∅ ↔ A = ∅ ∧ B ≠ ∅
Proof
Step
Hyp
Ref
Expression
1
map0.1 ⊢ A ∈ V
2
map0.2 ⊢ B ∈ V
3
map0g ⊢ A ∈ V ∧ B ∈ V → A B = ∅ ↔ A = ∅ ∧ B ≠ ∅
4
1 2 3
mp2an ⊢ A B = ∅ ↔ A = ∅ ∧ B ≠ ∅