Theorem eqimss2i 4011

Description: Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)

Hypothesis

Ref	Expression
eqimssi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eqimss2i	⊢ 𝐵 ⊆ 𝐴

Proof of Theorem eqimss2i

Step	Hyp	Ref	Expression
1		ssid 3972	. 2 ⊢ 𝐵 ⊆ 𝐵
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtrri 3999	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  cotr3  14951  supcvg  15829  prodfclim1  15866  ef0lem  16051  1strbas  17201  restid  17403  cayley  19351  gsumval3  19844  gsumzaddlem  19858  kgencn3  23452  hmeores  23665  opnfbas  23736  tsmsf1o  24039  ust0  24114  icchmeo  24845  icchmeoOLD  24846  plyeq0lem  26122  ulmdvlem1  26316  basellem7  27004  basellem9  27006  dchrisumlem3  27409  structvtxvallem  28954  struct2griedg  28962  gsumhashmul  33008  cycpmfvlem  33076  cycpmfv3  33079  constr01  33739  ivthALT  36330  aomclem4  43053  hashnzfzclim  44318  binomcxplemrat  44346  climsuselem1  45612  gsumfsupp  48174