Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Replacement
Theorems requiring subset and intersection existence
ssexi
Next ⟩
ssexg
Metamath Proof Explorer
Ascii
Unicode
Theorem
ssexi
Description:
The subset of a set is also a set.
(Contributed by
NM
, 9-Sep-1993)
Ref
Expression
Hypotheses
ssexi.1
⊢
B
∈
V
ssexi.2
⊢
A
⊆
B
Assertion
ssexi
⊢
A
∈
V
Proof
Step
Hyp
Ref
Expression
1
ssexi.1
⊢
B
∈
V
2
ssexi.2
⊢
A
⊆
B
3
1
ssex
⊢
A
⊆
B
→
A
∈
V
4
2
3
ax-mp
⊢
A
∈
V