Theorem eqsstrrd 3958

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  3sstr3d  3977  ssxpb  6133  fnsnr  7112  suppssof1  8143  oaword1  8481  omword2  8503  oeeui  8532  nnaword1  8559  naddword1  8621  naddunif  8623  cantnfle  9586  cantnflem1d  9603  r1val1  9704  rankr1id  9780  rankxplim3  9799  ackbij2  10158  ttukeylem7  10431  gruima  10719  hashdmpropge2  14439  rlimi  15469  rlimi2  15470  lo1bdd  15476  o1bdd  15487  rlimuni  15506  rlimcld2  15534  o1co  15542  rlimcn1  15544  rlimcn3  15546  o1add2  15580  o1mul2  15581  o1sub2  15582  lo1add  15583  lo1mul  15584  o1dif  15586  rlimneg  15603  rlimsqzlem  15605  lo1le  15608  rlimno1  15610  ramub1lem1  16991  imasaddfnlem  17486  imasvscafn  17495  mrcidb  17575  mrieqv2d  17599  mreexexlem4d  17607  funcres  17857  funcsetcres2  18054  acsfiindd  18513  tsrdir  18564  resmgmhm2  18674  resmhm2  18783  ghmqusnsg  19251  ghmquskerlem3  19255  ghmqusker  19256  f1omvdco2  19417  sylow2a  19588  sylow3lem6  19601  dprdspan  19998  dprd2dlem2  20011  dprd2dlem1  20012  dprd2da  20013  dmdprdsplit2lem  20016  dprdsplit  20019  dpjcntz  20023  ablfac1eu  20044  ringidss  20252  subrg1  20553  subrgdvds  20557  subrguss  20558  subrginv  20559  drngdomn  20720  subdrgint  20774  primefld  20776  islss3  20948  lspsnneg  20995  lspextmo  21046  lspsnvs  21107  lsmcv  21134  islbs3  21148  rhmqusnsg  21278  f1lindf  21815  psrbaglesupp  21915  resspsrbas  21965  resspsradd  21966  resspsrmul  21967  evlseu  22074  evlsvvval  22084  epttop  22987  neitr  23158  ordtbas  23170  ordtrest2  23182  pnfnei  23198  mnfnei  23199  ordtrestixx  23200  dnsconst  23356  cmpcld  23380  txindis  23612  txtube  23618  xkohaus  23631  xkopt  23633  xkococnlem  23637  xkoinjcn  23665  qtopval2  23674  ssufl  23896  ufldom  23940  cnextcn  24045  tmdgsum2  24074  clssubg  24087  clsnsg  24088  ustund  24200  ustneism  24202  trust  24207  fmucnd  24269  imasdsf1olem  24351  setsmstopn  24456  metequiv2  24488  metust  24536  restmetu  24548  tngtopn  24628  xlebnum  24945  pi1xfrcnv  25037  limcdif  25856  limccnp  25871  limccnp2  25872  limcco  25873  dvn2bss  25910  cpnord  25915  dvcmulf  25925  dvmptres2  25942  dvmptcmul  25944  dvmptntr  25951  dvcnvrelem2  25998  dvcnvre  25999  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem3  26383  psercnlem2  26405  rlimcxp  26954  o1cxp  26955  nosupbnd2lem1  27696  noinfbnd2lem1  27711  noetainflem4  27721  bdayiun  27924  negbday  28066  bdaypw2n0bndlem  28472  bdaypw2bnd  28474  bdayfinbndlem1  28476  sspg  30817  ssps  30819  sspn  30825  mdslj1i  32408  mdslj2i  32409  sh1dle  32440  shatomistici  32450  sumdmdii  32504  prssad  32617  prssbd  32618  unidifsnel  32623  tpssad  32627  fisuppov1  32774  resf1o  32821  gsumpart  33142  gsumhashmul  33146  symgcom2  33163  submarchi  33265  nsgmgc  33490  lmhmqusker  33495  rhmquskerlem  33503  idlinsubrg  33509  ressply1evls1  33643  esplyind  33737  ply1degltdimlem  33785  fedgmullem1  33792  fedgmullem2  33793  fedgmul  33794  extdg1id  33829  fldextrspunlem1  33838  madjusmdetlem1  33990  txomap  33997  rspectopn  34030  zarclssn  34036  zarcmplem  34044  cnvordtrestixx  34076  dya2iocucvr  34447  carsggect  34481  bnj1241  34968  bnj906  35091  fineqvac  35279  cvmscld  35474  fvline2  36347  cldregopn  36532  ttcwf2  36726  pibt2  37750  poimirlem15  37973  sstotbnd2  38112  totbndbnd  38127  heibor1  38148  heiborlem8  38156  lsmsat  39471  lssats  39475  lkrpssN  39626  dia2dimlem5  41531  cdlemn2a  41659  dihglblem6  41803  dochocsp  41842  dochdmj1  41853  dochsatshpb  41915  lcfl9a  41968  lclkrlem2r  41987  lclkrlem2s  41988  lclkrlem2v  41991  lcfrlem6  42010  lcfrlem25  42030  lcfrlem35  42040  mapdval2N  42093  mapdin  42125  baerlem5alem2  42174  baerlem5blem2  42175  evlsbagval  43019  evlsmhpvvval  43045  mhphf  43047  dnnumch2  43494  oege1  43755  omabs2  43781  nadd2rabex  43835  clrellem  44070  iunrelexpmin1  44156  iunrelexpmin2  44160  dftrcl3  44168  brtrclfv2  44175  dfrtrcl3  44181  mnuprdlem1  44720  mnuprdlem2  44721  mullimc  46067  islptre  46070  mullimcf  46074  limcmptdm  46084  dvresntr  46367  itgperiod  46430  fourierdlem89  46644  fourierdlem91  46646  iccpartgt  47902  clnbgrgrim  48425  setrecsres  50192