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
Unicode
Theorem
ssidd
Description:
Weakening of
ssid
.
(Contributed by
BJ
, 1-Sep-2022)
Ref
Expression
Assertion
ssidd
⊢
φ
→
A
⊆
A
Proof
Step
Hyp
Ref
Expression
1
ssid
⊢
A
⊆
A
2
1
a1i
⊢
φ
→
A
⊆
A