Theorem eqsstrrd 3969

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  3sstr3d  3988  ssxpb  6132  fnsnr  7109  suppssof1  8141  oaword1  8479  omword2  8501  oeeui  8530  nnaword1  8557  naddword1  8619  naddunif  8621  cantnfle  9580  cantnflem1d  9597  r1val1  9698  rankr1id  9774  rankxplim3  9793  ackbij2  10152  ttukeylem7  10425  gruima  10713  hashdmpropge2  14406  rlimi  15436  rlimi2  15437  lo1bdd  15443  o1bdd  15454  rlimuni  15473  rlimcld2  15501  o1co  15509  rlimcn1  15511  rlimcn3  15513  o1add2  15547  o1mul2  15548  o1sub2  15549  lo1add  15550  lo1mul  15551  o1dif  15553  rlimneg  15570  rlimsqzlem  15572  lo1le  15575  rlimno1  15577  ramub1lem1  16954  imasaddfnlem  17449  imasvscafn  17458  mrcidb  17538  mrieqv2d  17562  mreexexlem4d  17570  funcres  17820  funcsetcres2  18017  acsfiindd  18476  tsrdir  18527  resmgmhm2  18637  resmhm2  18746  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  f1omvdco2  19377  sylow2a  19548  sylow3lem6  19561  dprdspan  19958  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  dprdsplit  19979  dpjcntz  19983  ablfac1eu  20004  ringidss  20212  subrg1  20515  subrgdvds  20519  subrguss  20520  subrginv  20521  drngdomn  20682  subdrgint  20736  primefld  20738  islss3  20910  lspsnneg  20957  lspextmo  21008  lspsnvs  21069  lsmcv  21096  islbs3  21110  rhmqusnsg  21240  f1lindf  21777  psrbaglesupp  21878  resspsrbas  21929  resspsradd  21930  resspsrmul  21931  evlseu  22038  evlsvvval  22048  epttop  22953  neitr  23124  ordtbas  23136  ordtrest2  23148  pnfnei  23164  mnfnei  23165  ordtrestixx  23166  dnsconst  23322  cmpcld  23346  txindis  23578  txtube  23584  xkohaus  23597  xkopt  23599  xkococnlem  23603  xkoinjcn  23631  qtopval2  23640  ssufl  23862  ufldom  23906  cnextcn  24011  tmdgsum2  24040  clssubg  24053  clsnsg  24054  ustund  24166  ustneism  24168  trust  24173  fmucnd  24235  imasdsf1olem  24317  setsmstopn  24422  metequiv2  24454  metust  24502  restmetu  24514  tngtopn  24594  xlebnum  24920  pi1xfrcnv  25013  limcdif  25833  limccnp  25848  limccnp2  25849  limcco  25850  dvn2bss  25888  cpnord  25893  dvcmulf  25904  dvmptres2  25922  dvmptcmul  25924  dvmptntr  25931  dvcnvrelem2  25979  dvcnvre  25980  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem3  26367  psercnlem2  26390  rlimcxp  26940  o1cxp  26941  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetainflem4  27708  bdayiun  27911  negbday  28053  bdaypw2n0bndlem  28459  bdaypw2bnd  28461  bdayfinbndlem1  28463  sspg  30803  ssps  30805  sspn  30811  mdslj1i  32394  mdslj2i  32395  sh1dle  32426  shatomistici  32436  sumdmdii  32490  prssad  32604  prssbd  32605  unidifsnel  32610  tpssad  32614  fisuppov1  32762  resf1o  32809  gsumpart  33146  gsumhashmul  33150  symgcom2  33166  submarchi  33268  nsgmgc  33493  lmhmqusker  33498  rhmquskerlem  33506  idlinsubrg  33512  ressply1evls1  33646  esplyind  33731  ply1degltdimlem  33779  fedgmullem1  33786  fedgmullem2  33787  fedgmul  33788  extdg1id  33823  fldextrspunlem1  33832  madjusmdetlem1  33984  txomap  33991  rspectopn  34024  zarclssn  34030  zarcmplem  34038  cnvordtrestixx  34070  dya2iocucvr  34441  carsggect  34475  bnj1241  34963  bnj906  35086  fineqvac  35272  cvmscld  35467  fvline2  36340  cldregopn  36525  pibt2  37618  poimirlem15  37832  sstotbnd2  37971  totbndbnd  37986  heibor1  38007  heiborlem8  38015  lsmsat  39264  lssats  39268  lkrpssN  39419  dia2dimlem5  41324  cdlemn2a  41452  dihglblem6  41596  dochocsp  41635  dochdmj1  41646  dochsatshpb  41708  lcfl9a  41761  lclkrlem2r  41780  lclkrlem2s  41781  lclkrlem2v  41784  lcfrlem6  41803  lcfrlem25  41823  lcfrlem35  41833  mapdval2N  41886  mapdin  41918  baerlem5alem2  41967  baerlem5blem2  41968  evlsbagval  42808  evlsmhpvvval  42834  mhphf  42836  dnnumch2  43283  oege1  43544  omabs2  43570  nadd2rabex  43624  clrellem  43859  iunrelexpmin1  43945  iunrelexpmin2  43949  dftrcl3  43957  brtrclfv2  43964  dfrtrcl3  43970  mnuprdlem1  44509  mnuprdlem2  44510  mullimc  45858  islptre  45861  mullimcf  45865  limcmptdm  45875  dvresntr  46158  itgperiod  46221  fourierdlem89  46435  fourierdlem91  46437  iccpartgt  47669  clnbgrgrim  48176  setrecsres  49943