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

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

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 3920

This theorem is referenced by:  3sstr3d  3990  ssxpb  6140  fnsnr  7119  suppssof1  8151  oaword1  8489  omword2  8511  oeeui  8540  nnaword1  8567  naddword1  8629  naddunif  8631  cantnfle  9592  cantnflem1d  9609  r1val1  9710  rankr1id  9786  rankxplim3  9805  ackbij2  10164  ttukeylem7  10437  gruima  10725  hashdmpropge2  14418  rlimi  15448  rlimi2  15449  lo1bdd  15455  o1bdd  15466  rlimuni  15485  rlimcld2  15513  o1co  15521  rlimcn1  15523  rlimcn3  15525  o1add2  15559  o1mul2  15560  o1sub2  15561  lo1add  15562  lo1mul  15563  o1dif  15565  rlimneg  15582  rlimsqzlem  15584  lo1le  15587  rlimno1  15589  ramub1lem1  16966  imasaddfnlem  17461  imasvscafn  17470  mrcidb  17550  mrieqv2d  17574  mreexexlem4d  17582  funcres  17832  funcsetcres2  18029  acsfiindd  18488  tsrdir  18539  resmgmhm2  18649  resmhm2  18758  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  f1omvdco2  19389  sylow2a  19560  sylow3lem6  19573  dprdspan  19970  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  dprdsplit  19991  dpjcntz  19995  ablfac1eu  20016  ringidss  20224  subrg1  20527  subrgdvds  20531  subrguss  20532  subrginv  20533  drngdomn  20694  subdrgint  20748  primefld  20750  islss3  20922  lspsnneg  20969  lspextmo  21020  lspsnvs  21081  lsmcv  21108  islbs3  21122  rhmqusnsg  21252  f1lindf  21789  psrbaglesupp  21890  resspsrbas  21941  resspsradd  21942  resspsrmul  21943  evlseu  22050  evlsvvval  22060  epttop  22965  neitr  23136  ordtbas  23148  ordtrest2  23160  pnfnei  23176  mnfnei  23177  ordtrestixx  23178  dnsconst  23334  cmpcld  23358  txindis  23590  txtube  23596  xkohaus  23609  xkopt  23611  xkococnlem  23615  xkoinjcn  23643  qtopval2  23652  ssufl  23874  ufldom  23918  cnextcn  24023  tmdgsum2  24052  clssubg  24065  clsnsg  24066  ustund  24178  ustneism  24180  trust  24185  fmucnd  24247  imasdsf1olem  24329  setsmstopn  24434  metequiv2  24466  metust  24514  restmetu  24526  tngtopn  24606  xlebnum  24932  pi1xfrcnv  25025  limcdif  25845  limccnp  25860  limccnp2  25861  limcco  25862  dvn2bss  25900  cpnord  25905  dvcmulf  25916  dvmptres2  25934  dvmptcmul  25936  dvmptntr  25943  dvcnvrelem2  25991  dvcnvre  25992  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem3  26379  psercnlem2  26402  rlimcxp  26952  o1cxp  26953  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetainflem4  27720  bdayiun  27923  negbday  28065  bdaypw2n0bndlem  28471  bdaypw2bnd  28473  bdayfinbndlem1  28475  sspg  30816  ssps  30818  sspn  30824  mdslj1i  32407  mdslj2i  32408  sh1dle  32439  shatomistici  32449  sumdmdii  32503  prssad  32616  prssbd  32617  unidifsnel  32622  tpssad  32626  fisuppov1  32773  resf1o  32820  gsumpart  33157  gsumhashmul  33161  symgcom2  33178  submarchi  33280  nsgmgc  33505  lmhmqusker  33510  rhmquskerlem  33518  idlinsubrg  33524  ressply1evls1  33658  esplyind  33752  ply1degltdimlem  33800  fedgmullem1  33807  fedgmullem2  33808  fedgmul  33809  extdg1id  33844  fldextrspunlem1  33853  madjusmdetlem1  34005  txomap  34012  rspectopn  34045  zarclssn  34051  zarcmplem  34059  cnvordtrestixx  34091  dya2iocucvr  34462  carsggect  34496  bnj1241  34983  bnj906  35106  fineqvac  35294  cvmscld  35489  fvline2  36362  cldregopn  36547  pibt2  37672  poimirlem15  37886  sstotbnd2  38025  totbndbnd  38040  heibor1  38061  heiborlem8  38069  lsmsat  39384  lssats  39388  lkrpssN  39539  dia2dimlem5  41444  cdlemn2a  41572  dihglblem6  41716  dochocsp  41755  dochdmj1  41766  dochsatshpb  41828  lcfl9a  41881  lclkrlem2r  41900  lclkrlem2s  41901  lclkrlem2v  41904  lcfrlem6  41923  lcfrlem25  41943  lcfrlem35  41953  mapdval2N  42006  mapdin  42038  baerlem5alem2  42087  baerlem5blem2  42088  evlsbagval  42927  evlsmhpvvval  42953  mhphf  42955  dnnumch2  43402  oege1  43663  omabs2  43689  nadd2rabex  43743  clrellem  43978  iunrelexpmin1  44064  iunrelexpmin2  44068  dftrcl3  44076  brtrclfv2  44083  dfrtrcl3  44089  mnuprdlem1  44628  mnuprdlem2  44629  mullimc  45976  islptre  45979  mullimcf  45983  limcmptdm  45993  dvresntr  46276  itgperiod  46339  fourierdlem89  46553  fourierdlem91  46555  iccpartgt  47787  clnbgrgrim  48294  setrecsres  50061