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