Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The union of a class
unisnv
Next ⟩
unisn3
Metamath Proof Explorer
Ascii
Structured
Theorem
unisnv
Description:
A set equals the union of its singleton (setvar case).
(Contributed by
NM
, 30-Aug-1993)
Ref
Expression
Assertion
unisnv
⊢
∪
{
𝑥
} =
𝑥
Proof
Step
Hyp
Ref
Expression
1
vex
⊢
𝑥
∈ V
2
1
unisn
⊢
∪
{
𝑥
} =
𝑥