Theorem eqimss2 3995

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

Assertion

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

Proof of Theorem eqimss2

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  pweq  4570  ifpprsnss  4723  unieq  4876  disjeq2  5071  disjeq1  5074  poeq2  5544  freq2  5600  seeq1  5602  seeq2  5603  dmcoeq  5938  xp11  6141  suc11  6434  funeq  6520  fimadmfoALT  6765  foco  6768  fconst3  7169  sorpssuni  7687  sorpssint  7688  tposeq  8180  oaass  8498  odi  8516  oen0  8524  mapssfset  8800  inficl  9340  fodomfi2  9982  zorng  10426  rlimclim  15481  imasaddfnlem  17461  imasvscafn  17470  gasubg  19243  pgpssslw  19555  dprddisj2  19982  dprd2da  19985  imadrhmcl  20742  evlslem6  22048  topgele  22886  topontopn  22896  connima  23381  islocfin  23473  ptbasfi  23537  txdis  23588  neifil  23836  elfm3  23906  rnelfmlem  23908  alexsubALTlem3  24005  alexsubALTlem4  24006  utopsnneiplem  24203  lmclimf  25272  uniiccdif  25547  dv11cn  25974  plypf1  26185  2pthon3v  30028  hstoh  32320  dmdi2  32392  disjeq1f  32660  eulerpartlemd  34544  rrvdmss  34627  umgr2cycllem  35356  refssfne  36574  neibastop3  36578  topmeet  36580  topjoin  36581  fnemeet2  36583  fnejoin1  36584  bj-restuni  37350  bj-inexeqex  37409  bj-idreseq  37417  heiborlem3  38064  funALTVeq  39036  disjeq  39085  lsatelbN  39382  lkrscss  39474  lshpset2N  39495  mapdrvallem2  42021  hdmaprnlem3eN  42234  hdmaplkr  42289  uneqsn  44381  ssrecnpr  44664  founiiun  45538  founiiun0  45549  caragendifcl  46872  fnfocofob  47439  imasetpreimafvbijlemfo  47765  iuneqconst2  49182  iineqconst2  49183  unilbeu  49344