Theorem eqsstrrd 3966

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  3sstr3d  3985  ssxpb  6166  fnsnr  7168  suppssof1  8216  oaword1  8560  omword2  8582  oeeui  8611  nnaword1  8638  naddword1  8701  naddunif  8703  cantnfle  9672  cantnflem1d  9689  r1val1  9793  rankr1id  9878  rankxplim3  9898  ackbij2  10320  ttukeylem7  10593  gruima  10887  hashdmpropge2  14628  rlimi  15680  rlimi2  15681  lo1bdd  15687  o1bdd  15698  rlimuni  15717  rlimcld2  15745  o1co  15753  rlimcn1  15755  rlimcn3  15757  o1add2  15791  o1mul2  15792  o1sub2  15793  lo1add  15794  lo1mul  15795  o1dif  15797  rlimneg  15814  rlimsqzlem  15816  lo1le  15819  rlimno1  15821  ramub1lem1  17204  imasaddfnlem  17700  imasvscafn  17709  mrcidb  17789  mrieqv2d  17813  mreexexlem4d  17821  funcres  18071  funcsetcres2  18268  acsfiindd  18727  tsrdir  18778  resmgmhm2  18901  resmhm2  19017  ghmqusnsg  19496  ghmquskerlem3  19500  ghmqusker  19501  f1omvdco2  19662  sylow2a  19833  sylow3lem6  19846  dprdspan  20243  dprd2dlem2  20256  dprd2dlem1  20257  dprd2da  20258  dmdprdsplit2lem  20261  dprdsplit  20264  dpjcntz  20268  ablfac1eu  20289  ringidss  20506  subrg1  20834  subrgdvds  20838  subrguss  20839  subrginv  20840  drngdomn  21003  subdrgint  21060  primefld  21062  islss3  21234  lspsnneg  21281  lspextmo  21331  lspsnvs  21392  lsmcv  21419  islbs3  21433  rhmqusnsg  21581  f1lindf  22128  psrbaglesupp  22230  resspsrbas  22281  resspsradd  22282  resspsrmul  22283  evlseu  22392  evlsvvval  22402  epttop  23327  neitr  23498  ordtbas  23510  ordtrest2  23522  pnfnei  23538  mnfnei  23539  ordtrestixx  23540  dnsconst  23696  cmpcld  23720  txindis  23953  txtube  23959  xkohaus  23972  xkopt  23974  xkococnlem  23978  xkoinjcn  24006  qtopval2  24015  ssufl  24237  ufldom  24281  cnextcn  24386  tmdgsum2  24415  clssubg  24428  clsnsg  24429  ustund  24541  ustneism  24543  trust  24548  fmucnd  24610  imasdsf1olem  24692  setsmstopn  24797  metequiv2  24829  metust  24877  restmetu  24889  tngtopn  24969  xlebnum  25286  pi1xfrcnv  25378  limcdif  26196  limccnp  26211  limccnp2  26212  limcco  26213  dvn2bss  26250  cpnord  26255  dvcmulf  26265  dvmptres2  26282  dvmptcmul  26284  dvmptntr  26291  dvcnvrelem2  26338  dvcnvre  26339  taylthlem1  26700  taylthlem2  26701  ulmdvlem3  26729  psercnlem2  26751  rlimcxp  27301  o1cxp  27302  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetainflem4  28097  bdayiun  28301  negbday  28443  bdaypw2n0bndlem  28849  bdaypw2bnd  28851  bdayfinbndlem1  28853  lnssplng  29270  prlngpln4  29436  sspg  31330  ssps  31332  sspn  31338  mdslj1i  32921  mdslj2i  32922  sh1dle  32953  shatomistici  32963  sumdmdii  33017  prssad  33125  prssbd  33126  unidifsnel  33131  tpssad  33135  fisuppov1  33276  resf1o  33322  gsumpart  33624  gsumhashmul  33628  symgcom2  33645  submarchi  33747  nsgmgc  33963  lmhmqusker  33968  rhmquskerlem  33975  idlinsubrg  33981  ressply1evls1  34097  esplyind  34207  ply1degltdimlem  34254  fedgmullem1  34261  fedgmullem2  34262  fedgmul  34263  extdg1id  34298  fldextrspunlem1  34307  madjusmdetlem1  34459  txomap  34466  rspectopn  34499  zarclssn  34505  zarcmplem  34513  cnvordtrestixx  34545  dya2iocucvr  34916  carsggect  34950  bnj1241  35437  bnj906  35560  fineqvac  35784  cvmscld  36038  fvline2  36911  cldregopn  37119  ttcwf2  37313  pibt2  38340  poimirlem15  38553  sstotbnd2  38708  totbndbnd  38723  heibor1  38744  heiborlem8  38752  lsmsat  40065  lssats  40069  lkrpssN  40220  dia2dimlem5  42125  cdlemn2a  42253  dihglblem6  42397  dochocsp  42436  dochdmj1  42447  dochsatshpb  42509  lcfl9a  42562  lclkrlem2r  42581  lclkrlem2s  42582  lclkrlem2v  42585  lcfrlem6  42604  lcfrlem25  42624  lcfrlem35  42634  mapdval2N  42687  mapdin  42719  baerlem5alem2  42768  baerlem5blem2  42769  evlsbagval  43614  evlsmhpvvval  43623  mhphf  43625  dnnumch2  44051  oege1  44307  omabs2  44333  nadd2rabex  44387  clrellem  44621  iunrelexpmin1  44707  iunrelexpmin2  44711  dftrcl3  44719  brtrclfv2  44726  dfrtrcl3  44732  mnuprdlem1  45255  mnuprdlem2  45256  mullimc  46627  islptre  46630  mullimcf  46634  limcmptdm  46644  dvresntr  46927  itgperiod  46990  fourierdlem89  47204  fourierdlem91  47206  iccpartgt  48508  clnbgrgrim  49031  setrecsres  50794