Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
eqimssd
Next ⟩
eqimsscd
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqimssd
Description:
Equality implies inclusion, deduction version.
(Contributed by
SN
, 6-Nov-2024)
Ref
Expression
Hypothesis
eqimssd.1
⊢
φ
→
A
=
B
Assertion
eqimssd
⊢
φ
→
A
⊆
B
Proof
Step
Hyp
Ref
Expression
1
eqimssd.1
⊢
φ
→
A
=
B
2
ssid
⊢
B
⊆
B
3
1
2
eqsstrdi
⊢
φ
→
A
⊆
B