eqimss2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem eqimss2 2100

Description: Equality implies the subclass relation.

**Assertion**
Ref	Expression
eqimss2

**Proof of Theorem eqimss2**
Step	Hyp	Ref	Expression
1		eqimss 2099	. 2
2	1	eqcoms 1470	1

Colors of variables: wff set class

Syntax hints:

wi 3

wceq 953

wss 2037

This theorem is referenced by: vss 2297 suc11 3083 dmcoeq 3350 xp11 3463 fconst3 3835 oaass 4179 odi 4194 oen0 4197 zorn 4769 subgres 8054 hstoht 10069

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-in 2041 df-ss 2043