Theorem eqimss2 4068

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

Assertion

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

Proof of Theorem eqimss2

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  pweq  4636  ifpprsnss  4789  unieq  4942  disjeq2  5137  disjeq1  5140  poeq2  5611  freq2  5668  seeq1  5670  seeq2  5671  dmcoeq  6001  xp11  6206  suc11  6502  funeq  6598  fimadmfoALT  6845  foco  6848  fconst3  7250  sorpssuni  7767  sorpssint  7768  tposeq  8269  oaass  8617  odi  8635  oen0  8642  mapssfset  8909  inficl  9494  fodomfi2  10129  zorng  10573  rlimclim  15592  imasaddfnlem  17588  imasvscafn  17597  gasubg  19342  pgpssslw  19656  dprddisj2  20083  dprd2da  20086  imadrhmcl  20820  evlslem6  22128  topgele  22957  topontopn  22967  connima  23454  islocfin  23546  ptbasfi  23610  txdis  23661  neifil  23909  elfm3  23979  rnelfmlem  23981  alexsubALTlem3  24078  alexsubALTlem4  24079  utopsnneiplem  24277  lmclimf  25357  uniiccdif  25632  dv11cn  26060  plypf1  26271  2pthon3v  29976  hstoh  32264  dmdi2  32336  disjeq1f  32595  eulerpartlemd  34331  rrvdmss  34414  umgr2cycllem  35108  refssfne  36324  neibastop3  36328  topmeet  36330  topjoin  36331  fnemeet2  36333  fnejoin1  36334  bj-restuni  37063  bj-inexeqex  37120  bj-idreseq  37128  heiborlem3  37773  funALTVeq  38656  disjeq  38690  lsatelbN  38962  lkrscss  39054  lshpset2N  39075  mapdrvallem2  41602  hdmaprnlem3eN  41815  hdmaplkr  41870  uneqsn  43987  ssrecnpr  44277  founiiun  45086  founiiun0  45097  caragendifcl  46435  fnfocofob  46994  imasetpreimafvbijlemfo  47279  unilbeu  48657