Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Utility theorems
pssexg
Next ⟩
pssn0
Metamath Proof Explorer
Ascii
Unicode
Theorem
pssexg
Description:
The proper subset of a set is also a set.
(Contributed by
Steven Nguyen
, 17-Jul-2022)
Ref
Expression
Assertion
pssexg
⊢
A
⊂
B
∧
B
∈
C
→
A
∈
V
Proof
Step
Hyp
Ref
Expression
1
pssss
⊢
A
⊂
B
→
A
⊆
B
2
ssexg
⊢
A
⊆
B
∧
B
∈
C
→
A
∈
V
3
1
2
sylan
⊢
A
⊂
B
∧
B
∈
C
→
A
∈
V