Theorem eqimss2 3944

Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)

Assertion

Ref	Expression
eqimss2	⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Proof of Theorem eqimss2

Step	Hyp	Ref	Expression
1		eqimss 3943	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	eqcoms 2744	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1543   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  pweq  4515  ifpprsnss  4666  unieq  4816  disjeq2  5008  disjeq1  5011  poeq2  5457  freq2  5507  seeq1  5508  seeq2  5509  dmcoeq  5828  xp11  6018  suc11  6294  funeq  6378  fimadmfoALT  6622  foco  6625  fconst3  7007  sorpssuni  7498  sorpssint  7499  tposeq  7948  oaass  8267  odi  8285  oen0  8292  mapssfset  8510  inficl  9019  fodomfi2  9639  zorng  10083  rlimclim  15072  imasaddfnlem  16987  imasvscafn  16996  gasubg  18650  pgpssslw  18957  dprddisj2  19380  dprd2da  19383  evlslem6  20995  topgele  21781  topontopn  21791  connima  22276  islocfin  22368  ptbasfi  22432  txdis  22483  neifil  22731  elfm3  22801  rnelfmlem  22803  alexsubALTlem3  22900  alexsubALTlem4  22901  utopsnneiplem  23099  lmclimf  24155  uniiccdif  24429  dv11cn  24852  plypf1  25060  2pthon3v  27981  hstoh  30267  dmdi2  30339  disjeq1f  30585  eulerpartlemd  31999  rrvdmss  32082  umgr2cycllem  32769  refssfne  34233  neibastop3  34237  topmeet  34239  topjoin  34240  fnemeet2  34242  fnejoin1  34243  bj-restuni  34952  bj-inexeqex  35009  bj-idreseq  35017  heiborlem3  35657  funALTVeq  36497  disjeq  36531  lsatelbN  36706  lkrscss  36798  lshpset2N  36819  mapdrvallem2  39345  hdmaprnlem3eN  39558  hdmaplkr  39613  uneqsn  41251  ssrecnpr  41540  founiiun  42329  founiiun0  42342  caragendifcl  43670  fnfocofob  44186  imasetpreimafvbijlemfo  44473  unilbeu  45887