Theorem eqsstrrd 3966

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  3sstr3d  3985  ssxpb  6167  fnsnr  7162  suppssof1  8198  oaword1  8540  omword2  8562  oeeui  8591  nnaword1  8618  naddword1  8681  naddunif  8683  cantnfle  9651  cantnflem1d  9668  r1val1  9769  rankr1id  9845  rankxplim3  9864  ackbij2  10245  ttukeylem7  10518  gruima  10812  hashdmpropge2  14549  rlimi  15601  rlimi2  15602  lo1bdd  15608  o1bdd  15619  rlimuni  15638  rlimcld2  15666  o1co  15674  rlimcn1  15676  rlimcn3  15678  o1add2  15712  o1mul2  15713  o1sub2  15714  lo1add  15715  lo1mul  15716  o1dif  15718  rlimneg  15735  rlimsqzlem  15737  lo1le  15740  rlimno1  15742  ramub1lem1  17119  imasaddfnlem  17615  imasvscafn  17624  mrcidb  17704  mrieqv2d  17728  mreexexlem4d  17736  funcres  17986  funcsetcres2  18183  acsfiindd  18642  tsrdir  18693  resmgmhm2  18815  resmhm2  18931  ghmqusnsg  19410  ghmquskerlem3  19414  ghmqusker  19415  f1omvdco2  19576  sylow2a  19747  sylow3lem6  19760  dprdspan  20157  dprd2dlem2  20170  dprd2dlem1  20171  dprd2da  20172  dmdprdsplit2lem  20175  dprdsplit  20178  dpjcntz  20182  ablfac1eu  20203  ringidss  20419  subrg1  20745  subrgdvds  20749  subrguss  20750  subrginv  20751  drngdomn  20913  subdrgint  20970  primefld  20972  islss3  21144  lspsnneg  21191  lspextmo  21241  lspsnvs  21302  lsmcv  21329  islbs3  21343  rhmqusnsg  21489  f1lindf  22036  psrbaglesupp  22138  resspsrbas  22189  resspsradd  22190  resspsrmul  22191  evlseu  22300  evlsvvval  22310  epttop  23235  neitr  23406  ordtbas  23418  ordtrest2  23430  pnfnei  23446  mnfnei  23447  ordtrestixx  23448  dnsconst  23604  cmpcld  23628  txindis  23861  txtube  23867  xkohaus  23880  xkopt  23882  xkococnlem  23886  xkoinjcn  23914  qtopval2  23923  ssufl  24145  ufldom  24189  cnextcn  24294  tmdgsum2  24323  clssubg  24336  clsnsg  24337  ustund  24449  ustneism  24451  trust  24456  fmucnd  24518  imasdsf1olem  24600  setsmstopn  24705  metequiv2  24737  metust  24785  restmetu  24797  tngtopn  24877  xlebnum  25194  pi1xfrcnv  25286  limcdif  26104  limccnp  26119  limccnp2  26120  limcco  26121  dvn2bss  26158  cpnord  26163  dvcmulf  26173  dvmptres2  26190  dvmptcmul  26192  dvmptntr  26199  dvcnvrelem2  26246  dvcnvre  26247  taylthlem1  26610  taylthlem2  26611  ulmdvlem3  26639  psercnlem2  26661  rlimcxp  27211  o1cxp  27212  nosupbnd2lem1  27952  noinfbnd2lem1  27967  noetainflem4  27977  bdayiun  28181  negbday  28323  bdaypw2n0bndlem  28729  bdaypw2bnd  28731  bdayfinbndlem1  28733  lnssplng  29150  prlngpln4  29316  sspg  31210  ssps  31212  sspn  31218  mdslj1i  32801  mdslj2i  32802  sh1dle  32833  shatomistici  32843  sumdmdii  32897  prssad  33005  prssbd  33006  unidifsnel  33011  tpssad  33015  fisuppov1  33156  resf1o  33202  gsumpart  33504  gsumhashmul  33508  symgcom2  33525  submarchi  33627  nsgmgc  33842  lmhmqusker  33847  rhmquskerlem  33854  idlinsubrg  33860  ressply1evls1  33976  esplyind  34086  ply1degltdimlem  34133  fedgmullem1  34140  fedgmullem2  34141  fedgmul  34142  extdg1id  34177  fldextrspunlem1  34186  madjusmdetlem1  34338  txomap  34345  rspectopn  34378  zarclssn  34384  zarcmplem  34392  cnvordtrestixx  34424  dya2iocucvr  34796  carsggect  34830  bnj1241  35317  bnj906  35440  fineqvac  35643  cvmscld  35853  fvline2  36727  cldregopn  36951  ttcwf2  37145  pibt2  38172  poimirlem15  38385  sstotbnd2  38525  totbndbnd  38540  heibor1  38561  heiborlem8  38569  lsmsat  39882  lssats  39886  lkrpssN  40037  dia2dimlem5  41942  cdlemn2a  42070  dihglblem6  42214  dochocsp  42253  dochdmj1  42264  dochsatshpb  42326  lcfl9a  42379  lclkrlem2r  42398  lclkrlem2s  42399  lclkrlem2v  42402  lcfrlem6  42421  lcfrlem25  42441  lcfrlem35  42451  mapdval2N  42504  mapdin  42536  baerlem5alem2  42585  baerlem5blem2  42586  evlsbagval  43433  evlsmhpvvval  43442  mhphf  43444  dnnumch2  43887  oege1  44148  omabs2  44174  nadd2rabex  44228  clrellem  44463  iunrelexpmin1  44549  iunrelexpmin2  44553  dftrcl3  44561  brtrclfv2  44568  dfrtrcl3  44574  mnuprdlem1  45097  mnuprdlem2  45098  mullimc  46447  islptre  46450  mullimcf  46454  limcmptdm  46464  dvresntr  46747  itgperiod  46810  fourierdlem89  47024  fourierdlem91  47026  iccpartgt  48328  clnbgrgrim  48851  setrecsres  50629