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  17552  mrieqv2d  17576  mreexexlem4d  17584  funcres  17834  funcsetcres2  18031  acsfiindd  18488  tsrdir  18539  resmgmhm2  18615  resmhm2  18724  ghmqusnsg  19190  ghmquskerlem3  19194  ghmqusker  19195  f1omvdco2  19354  sylow2a  19525  sylow3lem6  19538  dprdspan  19935  dprd2dlem2  19948  dprd2dlem1  19949  dprd2da  19950  dmdprdsplit2lem  19953  dprdsplit  19956  dpjcntz  19960  ablfac1eu  19981  ringidss  20162  subrg1  20467  subrgdvds  20471  subrguss  20472  subrginv  20473  drngdomn  20634  subdrgint  20688  primefld  20690  islss3  20841  lspsnneg  20888  lspextmo  20939  lspsnvs  21000  lsmcv  21027  islbs3  21041  rhmqusnsg  21171  f1lindf  21707  psrbaglesupp  21807  resspsrbas  21859  resspsradd  21860  resspsrmul  21861  evlseu  21966  epttop  22872  neitr  23043  ordtbas  23055  ordtrest2  23067  pnfnei  23083  mnfnei  23084  ordtrestixx  23085  dnsconst  23241  cmpcld  23265  txindis  23497  txtube  23503  xkohaus  23516  xkopt  23518  xkococnlem  23522  xkoinjcn  23550  qtopval2  23559  ssufl  23781  ufldom  23825  cnextcn  23930  tmdgsum2  23959  clssubg  23972  clsnsg  23973  ustund  24085  ustneism  24087  trust  24093  fmucnd  24155  imasdsf1olem  24237  setsmstopn  24342  metequiv2  24374  metust  24422  restmetu  24434  tngtopn  24514  xlebnum  24840  pi1xfrcnv  24933  limcdif  25753  limccnp  25768  limccnp2  25769  limcco  25770  dvn2bss  25808  cpnord  25813  dvcmulf  25824  dvmptres2  25842  dvmptcmul  25844  dvmptntr  25851  dvcnvrelem2  25899  dvcnvre  25900  taylthlem1  26257  taylthlem2  26258  taylthlem2OLD  26259  ulmdvlem3  26287  psercnlem2  26310  rlimcxp  26860  o1cxp  26861  nosupbnd2lem1  27603  noinfbnd2lem1  27618  noetainflem4  27628  negsbday  27939  sspg  30630  ssps  30632  sspn  30638  mdslj1i  32221  mdslj2i  32222  sh1dle  32253  shatomistici  32263  sumdmdii  32317  prssad  32431  prssbd  32432  unidifsnel  32437  tpssad  32441  fisuppov1  32579  resf1o  32626  gsumpart  32970  gsumhashmul  32974  symgcom2  33014  submarchi  33113  nsgmgc  33356  lmhmqusker  33361  rhmquskerlem  33369  idlinsubrg  33375  ressply1evls1  33507  ply1degltdimlem  33591  fedgmullem1  33598  fedgmullem2  33599  fedgmul  33600  extdg1id  33634  fldextrspunlem1  33643  madjusmdetlem1  33790  txomap  33797  rspectopn  33830  zarclssn  33836  zarcmplem  33844  cnvordtrestixx  33876  dya2iocucvr  34248  carsggect  34282  bnj1241  34770  bnj906  34893  fineqvac  35060  cvmscld  35233  fvline2  36107  cldregopn  36292  pibt2  37378  poimirlem15  37602  sstotbnd2  37741  totbndbnd  37756  heibor1  37777  heiborlem8  37785  lsmsat  38974  lssats  38978  lkrpssN  39129  dia2dimlem5  41035  cdlemn2a  41163  dihglblem6  41307  dochocsp  41346  dochdmj1  41357  dochsatshpb  41419  lcfl9a  41472  lclkrlem2r  41491  lclkrlem2s  41492  lclkrlem2v  41495  lcfrlem6  41514  lcfrlem25  41534  lcfrlem35  41544  mapdval2N  41597  mapdin  41629  baerlem5alem2  41678  baerlem5blem2  41679  evlsvvval  42524  evlsbagval  42527  evlsmhpvvval  42556  mhphf  42558  dnnumch2  43007  oege1  43268  omabs2  43294  nadd2rabex  43348  clrellem  43584  iunrelexpmin1  43670  iunrelexpmin2  43674  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  mnuprdlem1  44234  mnuprdlem2  44235  mullimc  45587  islptre  45590  mullimcf  45594  limcmptdm  45606  dvresntr  45889  itgperiod  45952  fourierdlem89  46166  fourierdlem91  46168  iccpartgt  47401  clnbgrgrim  47907  setrecsres  49664