Theorem eqimss2 4003

Description: Equality implies inclusion. (Contributed by NM, 23-Nov-2003.)

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  pweq  4573  ifpprsnss  4724  unieq  4878  disjeq2  5073  disjeq1  5076  poeq2  5543  freq2  5599  seeq1  5601  seeq2  5602  dmcoeq  5931  xp11  6136  suc11  6429  funeq  6520  fimadmfoALT  6765  foco  6768  fconst3  7169  sorpssuni  7688  sorpssint  7689  tposeq  8184  oaass  8502  odi  8520  oen0  8527  mapssfset  8801  inficl  9352  fodomfi2  9989  zorng  10433  rlimclim  15488  imasaddfnlem  17467  imasvscafn  17476  gasubg  19210  pgpssslw  19520  dprddisj2  19947  dprd2da  19950  imadrhmcl  20682  evlslem6  21964  topgele  22793  topontopn  22803  connima  23288  islocfin  23380  ptbasfi  23444  txdis  23495  neifil  23743  elfm3  23813  rnelfmlem  23815  alexsubALTlem3  23912  alexsubALTlem4  23913  utopsnneiplem  24111  lmclimf  25180  uniiccdif  25455  dv11cn  25882  plypf1  26093  2pthon3v  29846  hstoh  32134  dmdi2  32206  disjeq1f  32475  eulerpartlemd  34330  rrvdmss  34413  umgr2cycllem  35100  refssfne  36319  neibastop3  36323  topmeet  36325  topjoin  36326  fnemeet2  36328  fnejoin1  36329  bj-restuni  37058  bj-inexeqex  37115  bj-idreseq  37123  heiborlem3  37780  funALTVeq  38665  disjeq  38699  lsatelbN  38972  lkrscss  39064  lshpset2N  39085  mapdrvallem2  41612  hdmaprnlem3eN  41825  hdmaplkr  41880  uneqsn  43987  ssrecnpr  44270  founiiun  45146  founiiun0  45157  caragendifcl  46485  fnfocofob  47053  imasetpreimafvbijlemfo  47379  iuneqconst2  48784  iineqconst2  48785  unilbeu  48946