Theorem eqimss2 4024

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 4023	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 ⊆ 𝐵)
2	1	eqcoms 2829	1 ⊢ (𝐵 = 𝐴 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  pweq  4555  ifpprsnss  4700  unieq  4849  disjeq2  5035  disjeq1  5038  poeq2  5478  freq2  5526  seeq1  5527  seeq2  5528  dmcoeq  5845  xp11  6032  suc11  6294  funeq  6375  fimadmfoALT  6601  fconst3  6976  sorpssuni  7458  sorpssint  7459  tposeq  7894  oaass  8187  odi  8205  oen0  8212  inficl  8889  fodomfi2  9486  zorng  9926  rlimclim  14903  imasaddfnlem  16801  imasvscafn  16810  gasubg  18432  pgpssslw  18739  dprddisj2  19161  dprd2da  19164  evlslem6  20294  topgele  21538  topontopn  21548  connima  22033  islocfin  22125  ptbasfi  22189  txdis  22240  neifil  22488  elfm3  22558  rnelfmlem  22560  alexsubALTlem3  22657  alexsubALTlem4  22658  utopsnneiplem  22856  lmclimf  23907  uniiccdif  24179  dv11cn  24598  plypf1  24802  2pthon3v  27722  hstoh  30009  dmdi2  30081  disjeq1f  30323  eulerpartlemd  31624  rrvdmss  31707  umgr2cycllem  32387  refssfne  33706  neibastop3  33710  topmeet  33712  topjoin  33713  fnemeet2  33715  fnejoin1  33716  bj-restuni  34391  bj-inexeqex  34449  bj-idreseq  34457  heiborlem3  35106  funALTVeq  35948  disjeq  35982  lsatelbN  36157  lkrscss  36249  lshpset2N  36270  mapdrvallem2  38796  hdmaprnlem3eN  39009  hdmaplkr  39064  uneqsn  40393  ssrecnpr  40660  founiiun  41455  founiiun0  41471  caragendifcl  42816  imasetpreimafvbijlemfo  43585