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