Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
eqimss2
Next ⟩
eqimssi
Metamath Proof Explorer
Ascii
Structured
Theorem
eqimss2
Description:
Equality implies inclusion.
(Contributed by
NM
, 23-Nov-2003)
Ref
Expression
Assertion
eqimss2
⊢
(
𝐵
=
𝐴
→
𝐴
⊆
𝐵
)
Proof
Step
Hyp
Ref
Expression
1
eqimss
⊢
(
𝐴
=
𝐵
→
𝐴
⊆
𝐵
)
2
1
eqcoms
⊢
(
𝐵
=
𝐴
→
𝐴
⊆
𝐵
)