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  37622  poimirlem15  37836  sstotbnd2  37975  totbndbnd  37990  heibor1  38011  heiborlem8  38019  lsmsat  39268  lssats  39272  lkrpssN  39423  dia2dimlem5  41328  cdlemn2a  41456  dihglblem6  41600  dochocsp  41639  dochdmj1  41650  dochsatshpb  41712  lcfl9a  41765  lclkrlem2r  41784  lclkrlem2s  41785  lclkrlem2v  41788  lcfrlem6  41807  lcfrlem25  41827  lcfrlem35  41837  mapdval2N  41890  mapdin  41922  baerlem5alem2  41971  baerlem5blem2  41972  evlsbagval  42812  evlsmhpvvval  42838  mhphf  42840  dnnumch2  43287  oege1  43548  omabs2  43574  nadd2rabex  43628  clrellem  43863  iunrelexpmin1  43949  iunrelexpmin2  43953  dftrcl3  43961  brtrclfv2  43968  dfrtrcl3  43974  mnuprdlem1  44513  mnuprdlem2  44514  mullimc  45862  islptre  45865  mullimcf  45869  limcmptdm  45879  dvresntr  46162  itgperiod  46225  fourierdlem89  46439  fourierdlem91  46441  iccpartgt  47673  clnbgrgrim  48180  setrecsres  49947