Theorem eqimss2i 4070

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  cotr3  15027  supcvg  15904  prodfclim1  15941  ef0lem  16126  1strbas  17275  1strbasOLD  17276  restid  17493  cayley  19456  gsumval3  19949  gsumzaddlem  19963  kgencn3  23587  hmeores  23800  opnfbas  23871  tsmsf1o  24174  ust0  24249  icchmeo  24990  icchmeoOLD  24991  plyeq0lem  26269  ulmdvlem1  26461  basellem7  27148  basellem9  27150  dchrisumlem3  27553  structvtxvallem  29055  struct2griedg  29063  gsumhashmul  33040  cycpmfvlem  33105  cycpmfv3  33108  constr01  33732  ivthALT  36301  aomclem4  43014  hashnzfzclim  44291  binomcxplemrat  44319  climsuselem1  45528  gsumfsupp  47905