Theorem eqimss2i 3660

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

Hypothesis

Ref	Expression
eqimssi.1	|- A = B

Assertion

Ref	Expression
eqimss2i	|- B C_ A

Proof of Theorem eqimss2i

Step	Hyp	Ref	Expression
1		ssid 3624	. 2 |- B C_ B
2		eqimssi.1	. 2 |- A = B
3	1, 2	sseqtr4i 3638	1 |- B C_ A

Syntax hints:   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  cotr3  13717  supcvg  14588  prodfclim1  14625  ef0lem  14809  1strbas  15980  restid  16094  cayley  17834  gsumval3  18308  gsumzaddlem  18321  kgencn3  21361  hmeores  21574  opnfbas  21646  tsmsf1o  21948  ust0  22023  icchmeo  22740  plyeq0lem  23966  ulmdvlem1  24154  basellem7  24813  basellem9  24815  dchrisumlem3  25180  structvtxvallem  25909  struct2griedg  25920  ivthALT  32330  aomclem4  37627  hashnzfzclim  38521  binomcxplemrat  38549  climsuselem1  39839