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  19216  pgpssslw  19528  dprddisj2  19955  dprd2da  19958  imadrhmcl  20717  evlslem6  22021  topgele  22850  topontopn  22860  connima  23345  islocfin  23437  ptbasfi  23501  txdis  23552  neifil  23800  elfm3  23870  rnelfmlem  23872  alexsubALTlem3  23969  alexsubALTlem4  23970  utopsnneiplem  24168  lmclimf  25237  uniiccdif  25512  dv11cn  25939  plypf1  26150  2pthon3v  29923  hstoh  32211  dmdi2  32283  disjeq1f  32552  eulerpartlemd  34350  rrvdmss  34433  umgr2cycllem  35120  refssfne  36339  neibastop3  36343  topmeet  36345  topjoin  36346  fnemeet2  36348  fnejoin1  36349  bj-restuni  37078  bj-inexeqex  37135  bj-idreseq  37143  heiborlem3  37800  funALTVeq  38685  disjeq  38719  lsatelbN  38992  lkrscss  39084  lshpset2N  39105  mapdrvallem2  41632  hdmaprnlem3eN  41845  hdmaplkr  41900  uneqsn  44007  ssrecnpr  44290  founiiun  45166  founiiun0  45177  caragendifcl  46505  fnfocofob  47073  imasetpreimafvbijlemfo  47399  iuneqconst2  48804  iineqconst2  48805  unilbeu  48966