Theorem eqimss2 3972

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

Assertion

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

Proof of Theorem eqimss2

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  pweq  4574  ifpprsnss  4727  unieq  4883  disjeq2  5079  disjeq1  5082  poeq2  5570  freq2  5626  seeq1  5628  seeq2  5629  dmcoeq  5974  xp11  6185  suc11  6498  funeq  6587  fimadmfoALT  6837  foco  6840  fconst3  7250  sorpssuni  7780  sorpssint  7781  tposeq  8283  oaass  8607  odi  8625  oen0  8633  mapssfset  8911  inficl  9454  fodomfi2  10178  zorng  10621  rlimclim  15757  imasaddfnlem  17750  imasvscafn  17759  gasubg  19567  pgpssslw  19879  dprddisj2  20306  dprd2da  20309  imadrhmcl  21105  evlslem6  22445  topgele  23303  topontopn  23313  connima  23798  islocfin  23891  ptbasfi  23955  txdis  24006  neifil  24254  elfm3  24324  rnelfmlem  24326  alexsubALTlem3  24423  alexsubALTlem4  24424  utopsnneiplem  24621  lmclimf  25680  uniiccdif  25954  dv11cn  26376  plypf1  26586  2pthon3v  30589  umgr2cycllem  30803  hstoh  32891  dmdi2  32963  disjeq1f  33265  eulerpartlemd  35109  rrvdmss  35192  refssfne  37361  neibastop3  37365  topmeet  37367  topjoin  37368  fnemeet2  37370  fnejoin1  37371  bj-restuni  38288  bj-inexeqex  38343  bj-idreseq  38351  heiborlem3  39013  funALTVeq  39983  disjeq  40032  lsatelbN  40329  lkrscss  40421  lshpset2N  40442  mapdrvallem2  42968  hdmaprnlem3eN  43181  hdmaplkr  43236  uneqsn  45286  ssrecnpr  45553  founiiun  46467  founiiun0  46478  caragendifcl  47797  fnfocofob  48422  imasetpreimafvbijlemfo  48760  iuneqconst2  50265  iineqconst2  50266  unilbeu  50430