Theorem eqsstrrd 3979

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrrd.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrd

Step	Hyp	Ref	Expression
1		eqsstrrd.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2735	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3978	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:  3sstr3d  3998  ssxpb  6135  fnsnr  7119  suppssof1  8155  oaword1  8493  omword2  8515  oeeui  8543  nnaword1  8570  naddword1  8632  naddunif  8634  cantnfle  9600  cantnflem1d  9617  r1val1  9715  rankr1id  9791  rankxplim3  9810  ackbij2  10171  ttukeylem7  10444  gruima  10731  hashdmpropge2  14424  rlimi  15455  rlimi2  15456  lo1bdd  15462  o1bdd  15473  rlimuni  15492  rlimcld2  15520  o1co  15528  rlimcn1  15530  rlimcn3  15532  o1add2  15566  o1mul2  15567  o1sub2  15568  lo1add  15569  lo1mul  15570  o1dif  15572  rlimneg  15589  rlimsqzlem  15591  lo1le  15594  rlimno1  15596  ramub1lem1  16973  imasaddfnlem  17467  imasvscafn  17476  mrcidb  17556  mrieqv2d  17580  mreexexlem4d  17588  funcres  17838  funcsetcres2  18035  acsfiindd  18494  tsrdir  18545  resmgmhm2  18621  resmhm2  18730  ghmqusnsg  19196  ghmquskerlem3  19200  ghmqusker  19201  f1omvdco2  19362  sylow2a  19533  sylow3lem6  19546  dprdspan  19943  dprd2dlem2  19956  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  dprdsplit  19964  dpjcntz  19968  ablfac1eu  19989  ringidss  20197  subrg1  20502  subrgdvds  20506  subrguss  20507  subrginv  20508  drngdomn  20669  subdrgint  20723  primefld  20725  islss3  20897  lspsnneg  20944  lspextmo  20995  lspsnvs  21056  lsmcv  21083  islbs3  21097  rhmqusnsg  21227  f1lindf  21764  psrbaglesupp  21864  resspsrbas  21916  resspsradd  21917  resspsrmul  21918  evlseu  22023  epttop  22929  neitr  23100  ordtbas  23112  ordtrest2  23124  pnfnei  23140  mnfnei  23141  ordtrestixx  23142  dnsconst  23298  cmpcld  23322  txindis  23554  txtube  23560  xkohaus  23573  xkopt  23575  xkococnlem  23579  xkoinjcn  23607  qtopval2  23616  ssufl  23838  ufldom  23882  cnextcn  23987  tmdgsum2  24016  clssubg  24029  clsnsg  24030  ustund  24142  ustneism  24144  trust  24150  fmucnd  24212  imasdsf1olem  24294  setsmstopn  24399  metequiv2  24431  metust  24479  restmetu  24491  tngtopn  24571  xlebnum  24897  pi1xfrcnv  24990  limcdif  25810  limccnp  25825  limccnp2  25826  limcco  25827  dvn2bss  25865  cpnord  25870  dvcmulf  25881  dvmptres2  25899  dvmptcmul  25901  dvmptntr  25908  dvcnvrelem2  25956  dvcnvre  25957  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem3  26344  psercnlem2  26367  rlimcxp  26917  o1cxp  26918  nosupbnd2lem1  27660  noinfbnd2lem1  27675  noetainflem4  27685  bdayiun  27864  negsbday  28003  sspg  30707  ssps  30709  sspn  30715  mdslj1i  32298  mdslj2i  32299  sh1dle  32330  shatomistici  32340  sumdmdii  32394  prssad  32508  prssbd  32509  unidifsnel  32514  tpssad  32518  fisuppov1  32656  resf1o  32703  gsumpart  33040  gsumhashmul  33044  symgcom2  33056  submarchi  33155  nsgmgc  33376  lmhmqusker  33381  rhmquskerlem  33389  idlinsubrg  33395  ressply1evls1  33527  ply1degltdimlem  33611  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  extdg1id  33654  fldextrspunlem1  33663  madjusmdetlem1  33810  txomap  33817  rspectopn  33850  zarclssn  33856  zarcmplem  33864  cnvordtrestixx  33896  dya2iocucvr  34268  carsggect  34302  bnj1241  34790  bnj906  34913  fineqvac  35080  cvmscld  35253  fvline2  36127  cldregopn  36312  pibt2  37398  poimirlem15  37622  sstotbnd2  37761  totbndbnd  37776  heibor1  37797  heiborlem8  37805  lsmsat  38994  lssats  38998  lkrpssN  39149  dia2dimlem5  41055  cdlemn2a  41183  dihglblem6  41327  dochocsp  41366  dochdmj1  41377  dochsatshpb  41439  lcfl9a  41492  lclkrlem2r  41511  lclkrlem2s  41512  lclkrlem2v  41515  lcfrlem6  41534  lcfrlem25  41554  lcfrlem35  41564  mapdval2N  41617  mapdin  41649  baerlem5alem2  41698  baerlem5blem2  41699  evlsvvval  42544  evlsbagval  42547  evlsmhpvvval  42576  mhphf  42578  dnnumch2  43027  oege1  43288  omabs2  43314  nadd2rabex  43368  clrellem  43604  iunrelexpmin1  43690  iunrelexpmin2  43694  dftrcl3  43702  brtrclfv2  43709  dfrtrcl3  43715  mnuprdlem1  44254  mnuprdlem2  44255  mullimc  45607  islptre  45610  mullimcf  45614  limcmptdm  45626  dvresntr  45909  itgperiod  45972  fourierdlem89  46186  fourierdlem91  46188  iccpartgt  47421  clnbgrgrim  47927  setrecsres  49684