Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Subclasses and subsets
eqimssi
Next ⟩
eqimss2i
Metamath Proof Explorer
Ascii
Unicode
Theorem
eqimssi
Description:
Infer subclass relationship from equality.
(Contributed by
NM
, 6-Jan-2007)
Ref
Expression
Hypothesis
eqimssi.1
⊢
A
=
B
Assertion
eqimssi
⊢
A
⊆
B
Proof
Step
Hyp
Ref
Expression
1
eqimssi.1
⊢
A
=
B
2
ssid
⊢
A
⊆
A
3
2
1
sseqtri
⊢
A
⊆
B