Theorem eqsstrrd 3973

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 2771	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrd 3972	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

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

This theorem is used by:  3sstr3d  3992  ssxpb  6174  fnsnr  7167  suppssof1  8201  oaword1  8543  omword2  8565  oeeui  8594  nnaword1  8621  naddword1  8684  naddunif  8686  cantnfle  9647  cantnflem1d  9664  r1val1  9765  rankr1id  9841  rankxplim3  9860  ackbij2  10241  ttukeylem7  10514  gruima  10804  hashdmpropge2  14540  rlimi  15590  rlimi2  15591  lo1bdd  15597  o1bdd  15608  rlimuni  15627  rlimcld2  15655  o1co  15663  rlimcn1  15665  rlimcn3  15667  o1add2  15701  o1mul2  15702  o1sub2  15703  lo1add  15704  lo1mul  15705  o1dif  15707  rlimneg  15724  rlimsqzlem  15726  lo1le  15729  rlimno1  15731  ramub1lem1  17110  imasaddfnlem  17606  imasvscafn  17615  mrcidb  17695  mrieqv2d  17719  mreexexlem4d  17727  funcres  17977  funcsetcres2  18174  acsfiindd  18633  tsrdir  18684  resmgmhm2  18804  resmhm2  18919  ghmqusnsg  19398  ghmquskerlem3  19402  ghmqusker  19403  f1omvdco2  19564  sylow2a  19735  sylow3lem6  19748  dprdspan  20145  dprd2dlem2  20158  dprd2dlem1  20159  dprd2da  20160  dmdprdsplit2lem  20163  dprdsplit  20166  dpjcntz  20170  ablfac1eu  20191  ringidss  20407  subrg1  20733  subrgdvds  20737  subrguss  20738  subrginv  20739  drngdomn  20901  subdrgint  20958  primefld  20960  islss3  21132  lspsnneg  21179  lspextmo  21229  lspsnvs  21290  lsmcv  21317  islbs3  21331  rhmqusnsg  21477  f1lindf  22024  psrbaglesupp  22124  resspsrbas  22175  resspsradd  22176  resspsrmul  22177  evlseu  22286  evlsvvval  22296  epttop  23218  neitr  23389  ordtbas  23401  ordtrest2  23413  pnfnei  23429  mnfnei  23430  ordtrestixx  23431  dnsconst  23587  cmpcld  23611  txindis  23844  txtube  23850  xkohaus  23863  xkopt  23865  xkococnlem  23869  xkoinjcn  23897  qtopval2  23906  ssufl  24128  ufldom  24172  cnextcn  24277  tmdgsum2  24306  clssubg  24319  clsnsg  24320  ustund  24432  ustneism  24434  trust  24439  fmucnd  24501  imasdsf1olem  24583  setsmstopn  24688  metequiv2  24720  metust  24768  restmetu  24780  tngtopn  24860  xlebnum  25177  pi1xfrcnv  25269  limcdif  26088  limccnp  26103  limccnp2  26104  limcco  26105  dvn2bss  26142  cpnord  26147  dvcmulf  26157  dvmptres2  26174  dvmptcmul  26176  dvmptntr  26183  dvcnvrelem2  26230  dvcnvre  26231  taylthlem1  26589  taylthlem2  26590  ulmdvlem3  26618  psercnlem2  26640  rlimcxp  27191  o1cxp  27192  nosupbnd2lem1  27932  noinfbnd2lem1  27947  noetainflem4  27957  bdayiun  28161  negbday  28303  bdaypw2n0bndlem  28709  bdaypw2bnd  28711  bdayfinbndlem1  28713  lnssplng  29127  prlngpln4  29265  sspg  31153  ssps  31155  sspn  31161  mdslj1i  32744  mdslj2i  32745  sh1dle  32776  shatomistici  32786  sumdmdii  32840  prssad  32948  prssbd  32949  unidifsnel  32954  tpssad  32958  fisuppov1  33101  resf1o  33147  gsumpart  33449  gsumhashmul  33453  symgcom2  33470  submarchi  33572  nsgmgc  33787  lmhmqusker  33792  rhmquskerlem  33799  idlinsubrg  33805  ressply1evls1  33921  esplyind  34031  ply1degltdimlem  34078  fedgmullem1  34085  fedgmullem2  34086  fedgmul  34087  extdg1id  34122  fldextrspunlem1  34131  madjusmdetlem1  34283  txomap  34290  rspectopn  34323  zarclssn  34329  zarcmplem  34337  cnvordtrestixx  34369  dya2iocucvr  34741  carsggect  34775  bnj1241  35262  bnj906  35385  fineqvac  35588  cvmscld  35804  fvline2  36677  cldregopn  36901  ttcwf2  37095  pibt2  38122  poimirlem15  38345  sstotbnd2  38485  totbndbnd  38500  heibor1  38521  heiborlem8  38529  lsmsat  39842  lssats  39846  lkrpssN  39997  dia2dimlem5  41902  cdlemn2a  42030  dihglblem6  42174  dochocsp  42213  dochdmj1  42224  dochsatshpb  42286  lcfl9a  42339  lclkrlem2r  42358  lclkrlem2s  42359  lclkrlem2v  42362  lcfrlem6  42381  lcfrlem25  42401  lcfrlem35  42411  mapdval2N  42464  mapdin  42496  baerlem5alem2  42545  baerlem5blem2  42546  evlsbagval  43378  evlsmhpvvval  43387  mhphf  43389  dnnumch2  43832  oege1  44093  omabs2  44119  nadd2rabex  44173  clrellem  44408  iunrelexpmin1  44494  iunrelexpmin2  44498  dftrcl3  44506  brtrclfv2  44513  dfrtrcl3  44519  mnuprdlem1  45042  mnuprdlem2  45043  mullimc  46392  islptre  46395  mullimcf  46399  limcmptdm  46409  dvresntr  46692  itgperiod  46755  fourierdlem89  46969  fourierdlem91  46971  iccpartgt  48236  clnbgrgrim  48759  setrecsres  50539