Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Unordered and ordered pairs
prnz
Next ⟩
prnzg
Metamath Proof Explorer
Ascii
Unicode
Theorem
prnz
Description:
A pair containing a set is not empty.
(Contributed by
NM
, 9-Apr-1994)
Ref
Expression
Hypothesis
prnz.1
⊢
A
∈
V
Assertion
prnz
⊢
A
B
≠
∅
Proof
Step
Hyp
Ref
Expression
1
prnz.1
⊢
A
∈
V
2
1
prid1
⊢
A
∈
A
B
3
2
ne0ii
⊢
A
B
≠
∅