Theorem eqsstrrd 3972

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 3971	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  3sstr3d  3991  ssxpb  6172  fnsnr  7161  suppssof1  8191  oaword1  8533  omword2  8555  oeeui  8584  nnaword1  8611  naddword1  8674  naddunif  8676  cantnfle  9636  cantnflem1d  9653  r1val1  9754  rankr1id  9830  rankxplim3  9849  ackbij2  10221  ttukeylem7  10494  gruima  10782  hashdmpropge2  14516  rlimi  15560  rlimi2  15561  lo1bdd  15567  o1bdd  15578  rlimuni  15597  rlimcld2  15625  o1co  15633  rlimcn1  15635  rlimcn3  15637  o1add2  15671  o1mul2  15672  o1sub2  15673  lo1add  15674  lo1mul  15675  o1dif  15677  rlimneg  15694  rlimsqzlem  15696  lo1le  15699  rlimno1  15701  ramub1lem1  17081  imasaddfnlem  17577  imasvscafn  17586  mrcidb  17666  mrieqv2d  17690  mreexexlem4d  17698  funcres  17948  funcsetcres2  18145  acsfiindd  18604  tsrdir  18655  resmgmhm2  18765  resmhm2  18875  ghmqusnsg  19347  ghmquskerlem3  19351  ghmqusker  19352  f1omvdco2  19513  sylow2a  19684  sylow3lem6  19697  dprdspan  20094  dprd2dlem2  20107  dprd2dlem1  20108  dprd2da  20109  dmdprdsplit2lem  20112  dprdsplit  20115  dpjcntz  20119  ablfac1eu  20140  ringidss  20356  subrg1  20681  subrgdvds  20685  subrguss  20686  subrginv  20687  drngdomn  20849  subdrgint  20906  primefld  20908  islss3  21080  lspsnneg  21127  lspextmo  21177  lspsnvs  21238  lsmcv  21265  islbs3  21279  rhmqusnsg  21425  f1lindf  21972  psrbaglesupp  22072  resspsrbas  22123  resspsradd  22124  resspsrmul  22125  evlseu  22234  evlsvvval  22244  epttop  23166  neitr  23337  ordtbas  23349  ordtrest2  23361  pnfnei  23377  mnfnei  23378  ordtrestixx  23379  dnsconst  23535  cmpcld  23559  txindis  23791  txtube  23797  xkohaus  23810  xkopt  23812  xkococnlem  23816  xkoinjcn  23844  qtopval2  23853  ssufl  24075  ufldom  24119  cnextcn  24224  tmdgsum2  24253  clssubg  24266  clsnsg  24267  ustund  24379  ustneism  24381  trust  24386  fmucnd  24448  imasdsf1olem  24530  setsmstopn  24635  metequiv2  24667  metust  24715  restmetu  24727  tngtopn  24807  xlebnum  25124  pi1xfrcnv  25216  limcdif  26035  limccnp  26050  limccnp2  26051  limcco  26052  dvn2bss  26089  cpnord  26094  dvcmulf  26104  dvmptres2  26121  dvmptcmul  26123  dvmptntr  26130  dvcnvrelem2  26177  dvcnvre  26178  taylthlem1  26536  taylthlem2  26537  ulmdvlem3  26565  psercnlem2  26587  rlimcxp  27138  o1cxp  27139  nosupbnd2lem1  27879  noinfbnd2lem1  27894  noetainflem4  27904  bdayiun  28108  negbday  28250  bdaypw2n0bndlem  28656  bdaypw2bnd  28658  bdayfinbndlem1  28660  lnssplng  29074  prlngpln4  29208  sspg  31080  ssps  31082  sspn  31088  mdslj1i  32671  mdslj2i  32672  sh1dle  32703  shatomistici  32713  sumdmdii  32767  prssad  32875  prssbd  32876  unidifsnel  32881  tpssad  32885  fisuppov1  33028  resf1o  33075  gsumpart  33383  gsumhashmul  33387  symgcom2  33404  submarchi  33506  nsgmgc  33721  lmhmqusker  33726  rhmquskerlem  33733  idlinsubrg  33739  ressply1evls1  33855  esplyind  33965  ply1degltdimlem  34012  fedgmullem1  34019  fedgmullem2  34020  fedgmul  34021  extdg1id  34056  fldextrspunlem1  34065  madjusmdetlem1  34217  txomap  34224  rspectopn  34257  zarclssn  34263  zarcmplem  34271  cnvordtrestixx  34303  dya2iocucvr  34674  carsggect  34708  bnj1241  35195  bnj906  35318  fineqvac  35529  cvmscld  35765  fvline2  36638  cldregopn  36862  ttcwf2  37056  pibt2  38083  poimirlem15  38306  sstotbnd2  38445  totbndbnd  38460  heibor1  38481  heiborlem8  38489  lsmsat  39802  lssats  39806  lkrpssN  39957  dia2dimlem5  41862  cdlemn2a  41990  dihglblem6  42134  dochocsp  42173  dochdmj1  42184  dochsatshpb  42246  lcfl9a  42299  lclkrlem2r  42318  lclkrlem2s  42319  lclkrlem2v  42322  lcfrlem6  42341  lcfrlem25  42361  lcfrlem35  42371  mapdval2N  42424  mapdin  42456  baerlem5alem2  42505  baerlem5blem2  42506  evlsbagval  43338  evlsmhpvvval  43347  mhphf  43349  dnnumch2  43792  oege1  44053  omabs2  44079  nadd2rabex  44133  clrellem  44368  iunrelexpmin1  44454  iunrelexpmin2  44458  dftrcl3  44466  brtrclfv2  44473  dfrtrcl3  44479  mnuprdlem1  45002  mnuprdlem2  45003  mullimc  46352  islptre  46355  mullimcf  46359  limcmptdm  46369  dvresntr  46652  itgperiod  46715  fourierdlem89  46929  fourierdlem91  46931  iccpartgt  48196  clnbgrgrim  48719  setrecsres  50500