Theorem eqsstrrd 3948

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  3sstr3d  3967  ssxpb  6184  fnsnr  7200  suppssof1  8254  oaword1  8598  omword2  8620  oeeui  8649  nnaword1  8676  naddword1  8739  naddunif  8741  cantnfle  9709  cantnflem1d  9726  r1val1  9830  rankr1id  9915  rankxplim3  9935  ackbij2  10359  ttukeylem7  10632  gruima  10926  hashdmpropge2  14669  rlimi  15724  rlimi2  15725  lo1bdd  15731  o1bdd  15742  rlimuni  15761  rlimcld2  15789  o1co  15797  rlimcn1  15799  rlimcn3  15801  o1add2  15835  o1mul2  15836  o1sub2  15837  lo1add  15838  lo1mul  15839  o1dif  15841  rlimneg  15858  rlimsqzlem  15860  lo1le  15863  rlimno1  15865  ramub1lem1  17248  imasaddfnlem  17750  imasvscafn  17759  mrcidb  17839  mrieqv2d  17863  mreexexlem4d  17871  funcres  18121  funcsetcres2  18318  acsfiindd  18777  tsrdir  18828  resmgmhm2  18951  resmhm2  19067  ghmqusnsg  19547  ghmquskerlem3  19551  ghmqusker  19552  f1omvdco2  19713  sylow2a  19884  sylow3lem6  19897  dprdspan  20294  dprd2dlem2  20307  dprd2dlem1  20308  dprd2da  20309  dmdprdsplit2lem  20312  dprdsplit  20315  dpjcntz  20319  ablfac1eu  20340  ringidss  20557  subrg1  20885  subrgdvds  20889  subrguss  20890  subrginv  20891  drngdomn  21054  subdrgint  21111  primefld  21113  islss3  21285  lspsnneg  21332  lspextmo  21382  lspsnvs  21443  lsmcv  21470  islbs3  21484  rhmqusnsg  21632  f1lindf  22183  psrbaglesupp  22285  resspsrbas  22336  resspsradd  22337  resspsrmul  22338  evlseu  22447  evlsvvval  22457  epttop  23382  neitr  23553  ordtbas  23565  ordtrest2  23577  pnfnei  23593  mnfnei  23594  ordtrestixx  23595  dnsconst  23751  cmpcld  23775  txindis  24008  txtube  24014  xkohaus  24027  xkopt  24029  xkococnlem  24033  xkoinjcn  24061  qtopval2  24070  ssufl  24292  ufldom  24336  cnextcn  24441  tmdgsum2  24470  clssubg  24483  clsnsg  24484  ustund  24596  ustneism  24598  trust  24603  fmucnd  24665  imasdsf1olem  24747  setsmstopn  24852  metequiv2  24884  metust  24932  restmetu  24944  tngtopn  25024  xlebnum  25341  pi1xfrcnv  25433  limcdif  26251  limccnp  26266  limccnp2  26267  limcco  26268  dvn2bss  26305  cpnord  26310  dvcmulf  26320  dvmptres2  26337  dvmptcmul  26339  dvmptntr  26346  dvcnvrelem2  26393  dvcnvre  26394  taylthlem1  26757  taylthlem2  26758  ulmdvlem3  26786  psercnlem2  26808  rlimcxp  27358  o1cxp  27359  nosupbnd2lem1  28129  noinfbnd2lem1  28144  noetainflem4  28154  bdayiun  28358  negbday  28500  bdaypw2n0bndlem  28906  bdaypw2bnd  28908  bdayfinbndlem1  28910  lnssplng  29327  prlngpln4  29493  sspg  31387  ssps  31389  sspn  31395  mdslj1i  32978  mdslj2i  32979  sh1dle  33010  shatomistici  33020  sumdmdii  33074  prssad  33224  prssbd  33225  unidifsnel  33229  tpssad  33233  fisuppov1  33373  resf1o  33418  gsumpart  33723  gsumhashmul  33727  symgcom2  33744  submarchi  33846  nsgmgc  34067  lmhmqusker  34072  rhmquskerlem  34079  idlinsubrg  34085  ressply1evls1  34200  esplyind  34318  ply1degltdimlem  34365  fedgmullem1  34372  fedgmullem2  34373  fedgmul  34374  extdg1id  34409  fldextrspunlem1  34418  madjusmdetlem1  34570  txomap  34577  rspectopn  34610  zarclssn  34616  zarcmplem  34624  cnvordtrestixx  34656  dya2iocucvr  35027  carsggect  35061  bnj1241  35548  bnj906  35671  fineqvac  35925  cvmscld  36246  fvline2  37126  cldregopn  37334  ttcwf2  37528  nvo2  38229  pibt2  38608  poimirlem15  38821  sstotbnd2  38974  totbndbnd  38989  heibor1  39010  heiborlem8  39018  lsmsat  40331  lssats  40335  lkrpssN  40486  dia2dimlem5  42391  cdlemn2a  42519  dihglblem6  42663  dochocsp  42702  dochdmj1  42713  dochsatshpb  42775  lcfl9a  42828  lclkrlem2r  42847  lclkrlem2s  42848  lclkrlem2v  42851  lcfrlem6  42870  lcfrlem25  42890  lcfrlem35  42900  mapdval2N  42953  mapdin  42985  baerlem5alem2  43034  baerlem5blem2  43035  evlsbagval  43880  evlsmhpvvval  43889  mhphf  43891  dnnumch2  44318  oege1  44569  omabs2  44595  nadd2rabex  44649  clrellem  44883  iunrelexpmin1  44969  iunrelexpmin2  44973  dftrcl3  44981  brtrclfv2  44988  dfrtrcl3  44994  mnuprdlem1  45517  mnuprdlem2  45518  mullimc  46901  islptre  46904  mullimcf  46908  limcmptdm  46918  dvresntr  47201  itgperiod  47264  fourierdlem89  47478  fourierdlem91  47480  iccpartgt  48782  clnbgrgrim  49305  setrecsres  51201