Theorem eqsstrrd 3971

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

Syntax hints:   → wi 4   = wceq 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  3sstr3d  3990  ssxpb  6160  fnsnr  7147  suppssof1  8179  oaword1  8521  omword2  8543  oeeui  8572  nnaword1  8599  naddword1  8662  naddunif  8664  cantnfle  9626  cantnflem1d  9643  r1val1  9744  rankr1id  9820  rankxplim3  9839  ackbij2  10198  ttukeylem7  10472  gruima  10760  hashdmpropge2  14496  rlimi  15540  rlimi2  15541  lo1bdd  15547  o1bdd  15558  rlimuni  15577  rlimcld2  15605  o1co  15613  rlimcn1  15615  rlimcn3  15617  o1add2  15651  o1mul2  15652  o1sub2  15653  lo1add  15654  lo1mul  15655  o1dif  15657  rlimneg  15674  rlimsqzlem  15676  lo1le  15679  rlimno1  15681  ramub1lem1  17062  imasaddfnlem  17558  imasvscafn  17567  mrcidb  17647  mrieqv2d  17671  mreexexlem4d  17679  funcres  17929  funcsetcres2  18126  acsfiindd  18585  tsrdir  18636  resmgmhm2  18746  resmhm2  18855  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  f1omvdco2  19488  sylow2a  19659  sylow3lem6  19672  dprdspan  20069  dprd2dlem2  20082  dprd2dlem1  20083  dprd2da  20084  dmdprdsplit2lem  20087  dprdsplit  20090  dpjcntz  20094  ablfac1eu  20115  ringidss  20327  subrg1  20632  subrgdvds  20636  subrguss  20637  subrginv  20638  drngdomn  20799  subdrgint  20852  primefld  20854  islss3  21026  lspsnneg  21073  lspextmo  21123  lspsnvs  21184  lsmcv  21211  islbs3  21225  rhmqusnsg  21355  f1lindf  21874  psrbaglesupp  21974  resspsrbas  22025  resspsradd  22026  resspsrmul  22027  evlseu  22136  evlsvvval  22146  epttop  23069  neitr  23240  ordtbas  23252  ordtrest2  23264  pnfnei  23280  mnfnei  23281  ordtrestixx  23282  dnsconst  23438  cmpcld  23462  txindis  23694  txtube  23700  xkohaus  23713  xkopt  23715  xkococnlem  23719  xkoinjcn  23747  qtopval2  23756  ssufl  23978  ufldom  24022  cnextcn  24127  tmdgsum2  24156  clssubg  24169  clsnsg  24170  ustund  24282  ustneism  24284  trust  24289  fmucnd  24351  imasdsf1olem  24433  setsmstopn  24538  metequiv2  24570  metust  24618  restmetu  24630  tngtopn  24710  xlebnum  25027  pi1xfrcnv  25119  limcdif  25938  limccnp  25953  limccnp2  25954  limcco  25955  dvn2bss  25992  cpnord  25997  dvcmulf  26007  dvmptres2  26024  dvmptcmul  26026  dvmptntr  26033  dvcnvrelem2  26080  dvcnvre  26081  taylthlem1  26436  taylthlem2  26437  ulmdvlem3  26465  psercnlem2  26487  rlimcxp  27038  o1cxp  27039  nosupbnd2lem1  27779  noinfbnd2lem1  27794  noetainflem4  27804  bdayiun  28008  negbday  28150  bdaypw2n0bndlem  28556  bdaypw2bnd  28558  bdayfinbndlem1  28560  lnssplng  28999  sspg  30931  ssps  30933  sspn  30939  mdslj1i  32522  mdslj2i  32523  sh1dle  32554  shatomistici  32564  sumdmdii  32618  prssad  32728  prssbd  32729  unidifsnel  32734  tpssad  32738  fisuppov1  32885  resf1o  32932  gsumpart  33243  gsumhashmul  33247  symgcom2  33264  submarchi  33366  nsgmgc  33598  lmhmqusker  33603  rhmquskerlem  33611  idlinsubrg  33617  ressply1evls1  33761  esplyind  33872  ply1degltdimlem  33919  fedgmullem1  33926  fedgmullem2  33927  fedgmul  33928  extdg1id  33963  fldextrspunlem1  33972  madjusmdetlem1  34124  txomap  34131  rspectopn  34164  zarclssn  34170  zarcmplem  34178  cnvordtrestixx  34210  dya2iocucvr  34581  carsggect  34615  bnj1241  35102  bnj906  35225  fineqvac  35412  cvmscld  35623  fvline2  36496  cldregopn  36691  ttcwf2  36885  pibt2  37911  poimirlem15  38134  sstotbnd2  38273  totbndbnd  38288  heibor1  38309  heiborlem8  38317  lsmsat  39632  lssats  39636  lkrpssN  39787  dia2dimlem5  41692  cdlemn2a  41820  dihglblem6  41964  dochocsp  42003  dochdmj1  42014  dochsatshpb  42076  lcfl9a  42129  lclkrlem2r  42148  lclkrlem2s  42149  lclkrlem2v  42152  lcfrlem6  42171  lcfrlem25  42191  lcfrlem35  42201  mapdval2N  42254  mapdin  42286  baerlem5alem2  42335  baerlem5blem2  42336  evlsbagval  43168  evlsmhpvvval  43177  mhphf  43179  dnnumch2  43622  oege1  43883  omabs2  43909  nadd2rabex  43963  clrellem  44198  iunrelexpmin1  44284  iunrelexpmin2  44288  dftrcl3  44296  brtrclfv2  44303  dfrtrcl3  44309  mnuprdlem1  44848  mnuprdlem2  44849  mullimc  46192  islptre  46195  mullimcf  46199  limcmptdm  46209  dvresntr  46492  itgperiod  46555  fourierdlem89  46769  fourierdlem91  46771  iccpartgt  48033  clnbgrgrim  48556  setrecsres  50323