Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
ssv
Next ⟩
sseq1
Metamath Proof Explorer
Ascii
Structured
Theorem
ssv
Description:
Any class is a subclass of the universal class.
(Contributed by
NM
, 31-Oct-1995)
Ref
Expression
Assertion
ssv
⊢
𝐴
⊆ V
Proof
Step
Hyp
Ref
Expression
1
elex
⊢
(
𝑥
∈
𝐴
→
𝑥
∈ V )
2
1
ssriv
⊢
𝐴
⊆ V