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
Unicode
Theorem
eqimss2
Description:
Equality implies inclusion.
(Contributed by
NM
, 23-Nov-2003)
Ref
Expression
Assertion
eqimss2
⊢
B
=
A
→
A
⊆
B
Proof
Step
Hyp
Ref
Expression
1
eqimss
⊢
A
=
B
→
A
⊆
B
2
1
eqcoms
⊢
B
=
A
→
A
⊆
B