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
Unicode
Theorem
unisnv
Description:
A set equals the union of its singleton (setvar case).
(Contributed by
NM
, 30-Aug-1993)
Ref
Expression
Assertion
unisnv
⊢
⋃
x
=
x
Proof
Step
Hyp
Ref
Expression
1
vex
⊢
x
∈
V
2
1
unisn
⊢
⋃
x
=
x