Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
ssidd
Next ⟩
ssv
Metamath Proof Explorer
Ascii
Structured
Theorem
ssidd
Description:
Weakening of
ssid
.
(Contributed by
BJ
, 1-Sep-2022)
Ref
Expression
Assertion
ssidd
⊢
(
𝜑
→
𝐴
⊆
𝐴
)
Proof
Step
Hyp
Ref
Expression
1
ssid
⊢
𝐴
⊆
𝐴
2
1
a1i
⊢
(
𝜑
→
𝐴
⊆
𝐴
)