Theorem eqsstrrd 3957

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 3956	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 2708

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

This theorem is referenced by:  3sstr3d  3976  ssxpb  6138  fnsnr  7118  suppssof1  8149  oaword1  8487  omword2  8509  oeeui  8538  nnaword1  8565  naddword1  8627  naddunif  8629  cantnfle  9592  cantnflem1d  9609  r1val1  9710  rankr1id  9786  rankxplim3  9805  ackbij2  10164  ttukeylem7  10437  gruima  10725  hashdmpropge2  14445  rlimi  15475  rlimi2  15476  lo1bdd  15482  o1bdd  15493  rlimuni  15512  rlimcld2  15540  o1co  15548  rlimcn1  15550  rlimcn3  15552  o1add2  15586  o1mul2  15587  o1sub2  15588  lo1add  15589  lo1mul  15590  o1dif  15592  rlimneg  15609  rlimsqzlem  15611  lo1le  15614  rlimno1  15616  ramub1lem1  16997  imasaddfnlem  17492  imasvscafn  17501  mrcidb  17581  mrieqv2d  17605  mreexexlem4d  17613  funcres  17863  funcsetcres2  18060  acsfiindd  18519  tsrdir  18570  resmgmhm2  18680  resmhm2  18789  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  f1omvdco2  19423  sylow2a  19594  sylow3lem6  19607  dprdspan  20004  dprd2dlem2  20017  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  dprdsplit  20025  dpjcntz  20029  ablfac1eu  20050  ringidss  20258  subrg1  20559  subrgdvds  20563  subrguss  20564  subrginv  20565  drngdomn  20726  subdrgint  20780  primefld  20782  islss3  20954  lspsnneg  21001  lspextmo  21051  lspsnvs  21112  lsmcv  21139  islbs3  21153  rhmqusnsg  21283  f1lindf  21802  psrbaglesupp  21902  resspsrbas  21952  resspsradd  21953  resspsrmul  21954  evlseu  22061  evlsvvval  22071  epttop  22974  neitr  23145  ordtbas  23157  ordtrest2  23169  pnfnei  23185  mnfnei  23186  ordtrestixx  23187  dnsconst  23343  cmpcld  23367  txindis  23599  txtube  23605  xkohaus  23618  xkopt  23620  xkococnlem  23624  xkoinjcn  23652  qtopval2  23661  ssufl  23883  ufldom  23927  cnextcn  24032  tmdgsum2  24061  clssubg  24074  clsnsg  24075  ustund  24187  ustneism  24189  trust  24194  fmucnd  24256  imasdsf1olem  24338  setsmstopn  24443  metequiv2  24475  metust  24523  restmetu  24535  tngtopn  24615  xlebnum  24932  pi1xfrcnv  25024  limcdif  25843  limccnp  25858  limccnp2  25859  limcco  25860  dvn2bss  25897  cpnord  25902  dvcmulf  25912  dvmptres2  25929  dvmptcmul  25931  dvmptntr  25938  dvcnvrelem2  25985  dvcnvre  25986  taylthlem1  26338  taylthlem2  26339  ulmdvlem3  26367  psercnlem2  26389  rlimcxp  26937  o1cxp  26938  nosupbnd2lem1  27679  noinfbnd2lem1  27694  noetainflem4  27704  bdayiun  27907  negbday  28049  bdaypw2n0bndlem  28455  bdaypw2bnd  28457  bdayfinbndlem1  28459  sspg  30799  ssps  30801  sspn  30807  mdslj1i  32390  mdslj2i  32391  sh1dle  32422  shatomistici  32432  sumdmdii  32486  prssad  32599  prssbd  32600  unidifsnel  32605  tpssad  32609  fisuppov1  32756  resf1o  32803  gsumpart  33124  gsumhashmul  33128  symgcom2  33145  submarchi  33247  nsgmgc  33472  lmhmqusker  33477  rhmquskerlem  33485  idlinsubrg  33491  ressply1evls1  33625  esplyind  33719  ply1degltdimlem  33766  fedgmullem1  33773  fedgmullem2  33774  fedgmul  33775  extdg1id  33810  fldextrspunlem1  33819  madjusmdetlem1  33971  txomap  33978  rspectopn  34011  zarclssn  34017  zarcmplem  34025  cnvordtrestixx  34057  dya2iocucvr  34428  carsggect  34462  bnj1241  34949  bnj906  35072  fineqvac  35260  cvmscld  35455  fvline2  36328  cldregopn  36513  ttcwf2  36707  pibt2  37733  poimirlem15  37956  sstotbnd2  38095  totbndbnd  38110  heibor1  38131  heiborlem8  38139  lsmsat  39454  lssats  39458  lkrpssN  39609  dia2dimlem5  41514  cdlemn2a  41642  dihglblem6  41786  dochocsp  41825  dochdmj1  41836  dochsatshpb  41898  lcfl9a  41951  lclkrlem2r  41970  lclkrlem2s  41971  lclkrlem2v  41974  lcfrlem6  41993  lcfrlem25  42013  lcfrlem35  42023  mapdval2N  42076  mapdin  42108  baerlem5alem2  42157  baerlem5blem2  42158  evlsbagval  43002  evlsmhpvvval  43028  mhphf  43030  dnnumch2  43473  oege1  43734  omabs2  43760  nadd2rabex  43814  clrellem  44049  iunrelexpmin1  44135  iunrelexpmin2  44139  dftrcl3  44147  brtrclfv2  44154  dfrtrcl3  44160  mnuprdlem1  44699  mnuprdlem2  44700  mullimc  46046  islptre  46049  mullimcf  46053  limcmptdm  46063  dvresntr  46346  itgperiod  46409  fourierdlem89  46623  fourierdlem91  46625  iccpartgt  47887  clnbgrgrim  48410  setrecsres  50177