Theorem eqimss2i 4020

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 3981	. 2 ⊢ 𝐵 ⊆ 𝐵
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtrri 4008	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1540   ⊆ wss 3926

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  cotr3  14997  supcvg  15872  prodfclim1  15909  ef0lem  16094  1strbas  17244  1strbasOLD  17245  restid  17447  cayley  19395  gsumval3  19888  gsumzaddlem  19902  kgencn3  23496  hmeores  23709  opnfbas  23780  tsmsf1o  24083  ust0  24158  icchmeo  24889  icchmeoOLD  24890  plyeq0lem  26167  ulmdvlem1  26361  basellem7  27049  basellem9  27051  dchrisumlem3  27454  structvtxvallem  28999  struct2griedg  29007  gsumhashmul  33055  cycpmfvlem  33123  cycpmfv3  33126  constr01  33776  ivthALT  36353  aomclem4  43081  hashnzfzclim  44346  binomcxplemrat  44374  climsuselem1  45636  gsumfsupp  48157