Theorem rspcdva 3581

Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)

Hypotheses

Ref	Expression
rspcdva.1	⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
rspcdva.2	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
rspcdva.3	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
rspcdva	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rspcdva

Step	Hyp	Ref	Expression
1		rspcdva.3	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		rspcdva.2	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)
3		rspcdva.1	. . 3 ⊢ (𝑥 = 𝐶 → (𝜓 ↔ 𝜒))
4	3	rspcv 3576	. 2 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
5	1, 2, 4	sylc 65	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ∈ wcel 2141  ∀wral 3075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076

This theorem is referenced by:  nvocnv  7260  knatar  7336  caofref  7686  caofinvl  7687  tfisi  7834  frxp2  8118  frxp3  8125  suppssov1  8171  suppssov2  8172  fpr3g  8260  fprresex  8285  tfrlem1  8340  tfrlem5  8344  coflton  8635  cofon1  8636  cofon2  8637  marypha1lem  9373  marypha1  9374  ordtypelem6  9465  ordtypelem7  9466  wemaplem2  9489  oemapvali  9633  cantnflem1c  9636  ttrcltr  9665  ttrclss  9669  dmttrcl  9670  rnttrcl  9671  ttrclselem2  9675  infxpenlem  9963  acni  9995  dfac9  10087  dfac12lem2  10095  sornom  10228  fin1ai  10244  fin2i  10246  fin23lem11  10268  isfin2-2  10270  fin23lem17  10289  fin23lem39  10301  fin1a2lem13  10363  hsmexlem4  10380  ttukeylem5  10464  ttukeylem6  10465  canth4  10599  pwfseqlem5  10615  winalim2  10648  wununi  10658  wunpw  10659  dedekind  11340  zsupss  12932  uzwo3  12938  seqcl2  14027  seqcl  14029  seqf  14030  seqfveq2  14031  seqfveq  14033  seqshft2  14035  monoord  14039  monoord2  14040  sermono  14041  seqsplit  14042  seqcaopr3  14044  seqid  14054  seqid2  14055  seqhomo  14056  seqz  14057  discr1  14246  discr  14247  hashbclem  14459  wrdind  14729  limsupgre  15499  climi  15528  rlimi  15531  rlimclim1  15563  rlimclim  15564  climrlim2  15565  rlimcn1  15606  climcn1  15610  isercoll2  15687  caucvgrlem  15691  caucvgb  15698  iseraltlem2  15701  iseraltlem3  15702  fsumm1  15769  fsum1p  15771  fsumcom2  15792  fsumge1  15816  telfsumo  15821  telfsumo2  15822  fsumparts  15825  o1fsum  15832  isum1p  15862  isumnn0nn  15863  isumrpcl  15864  climcndslem1  15870  climcndslem2  15871  climcnds  15872  cvgrat  15904  mertenslem1  15905  mertens  15907  fprodm1  15988  fprod1p  15989  fprodcom2  16005  prmind2  16710  pcmpt2  16920  prmpwdvds  16931  prmreclem4  16946  prmreclem5  16947  vdwlem1  17008  vdwlem2  17009  vdwlem9  17016  vdwlem10  17017  rami  17042  ramcl  17056  prmodvdslcmf  17074  prmgaplcmlem1  17078  cshwsidrepsw  17120  prdsbasprj  17492  isacs2  17676  acsfiel  17677  catidex  17697  iscatd2  17704  catlid  17706  catrid  17707  subcidcl  17868  funcid  17894  yonedalem4c  18300  yonffthlem  18305  isdrs2  18329  luble  18380  glble  18393  joinle  18407  meetle  18421  poslubmo  18432  posglbmo  18433  acsdrsel  18566  isacs4lem  18567  isacs5lem  18568  acsdrscl  18569  acsficl  18570  chnltm1  18632  chnub  18645  lidrideqd  18694  grpinvalem  18698  grpinva  18699  mndind  18853  grpidd2  19010  mulgsubcl  19121  issubg4  19178  ghmf1  19277  fislw  19656  efgsdmi  19763  efgsrel  19765  gexexlem  19883  gsumzaddlem  19952  gsummhm2  19970  dprdcntz  20041  dprddisj  20042  dprdss  20062  dprd2dlem2  20073  dprd2da  20075  dpjrid  20095  ablfac1eu  20106  pgpfac1lem1  20107  pgpfaclem2  20115  lringuplu  20581  issrngd  20892  islbs2  21212  lbsextlem4  21219  prmirredlem  21512  psgndiflemB  21640  frlmphl  21821  mplsubglem  22038  mpllsslem  22039  subrgasclcl  22108  mplind  22111  evlslem1  22123  ply1scleq  22356  mdetralt  22656  mdetunilem1  22660  lmcvg  23310  iscncl  23317  lmff  23349  cnrmi  23408  cmpcov  23437  fiuncmp  23452  hauscmplem  23454  1stcfb  23493  1stcelcls  23509  restnlly  23530  islly2  23532  lly1stc  23544  kgeni  23585  ptpjpre1  23619  ptbasfi  23629  ptpjopn  23660  dfac14  23666  txtube  23688  cnmpt11  23711  cnmpt21  23719  cnmptkp  23728  cnmptk1p  23733  qtopomap  23766  qtopcmap  23767  flimcf  24030  fclscf  24073  flfcntr  24091  ptcmplem3  24102  tgpt0  24167  tsmsi  24182  tsmsxplem2  24202  tsmsxp  24203  isucn2  24326  ucnima  24328  ucncn  24332  cfiluweak  24342  cuspcvg  24348  imasdsf1olem  24421  lpbl  24551  comet  24561  cfilucfil  24607  cnheiborlem  25004  cnheibor  25005  bndth  25008  nmoleub2lem2  25166  nmoleub3  25169  ipcau2  25284  tcphcphlem1  25285  tcphcphlem2  25286  lmmcvg  25311  cmetcaulem  25338  iscmet3lem1  25341  iscmet3lem2  25342  pjthlem1  25487  pjthlem2  25488  ivthlem1  25501  ivthlem2  25502  ivthlem3  25503  ivth2  25505  ivthle  25506  ivthle2  25507  ivthicc  25508  ovoliunlem1  25552  ovolshftlem1  25559  ovolscalem1  25563  ovolicc2lem3  25569  ovolicc2lem4  25570  ovolicc2  25572  volsup  25606  dyadmbl  25650  vitalilem2  25659  vitalilem3  25660  mbfdm  25676  ismbf3d  25704  cncombf  25708  itg2seq  25792  itg2monolem2  25801  itg2monolem3  25802  itg2mono  25803  iblitg  25818  itgconst  25869  itgfsum  25877  limcvallem  25921  cnlimci  25939  cnmptlimc  25940  dvferm1lem  26034  dvferm1  26035  dvferm2lem  26036  dvferm2  26037  dvlipcn  26044  dvle  26057  lhop1lem  26063  dvfsumge  26072  dvfsumlem2  26077  dvfsumlem3  26078  ftc1a  26087  ftc1lem4  26089  itgsubstlem  26098  mdeglt  26113  deg1lt  26145  ply1divex  26185  fta1glem2  26217  fta1g  26218  plyco0  26240  plyeq0lem  26258  dgrcolem2  26322  plydivlem4  26348  plydivex  26349  fta1lem  26359  vieta1lem2  26363  vieta1  26364  tayl0  26413  ulmi  26437  ulmdvlem1  26451  ulmdvlem3  26453  ulmdv  26454  mtest  26455  pserulm  26473  efif1olem4  26598  rlimcnp  27018  rlimcnp2  27019  xrlimcnp  27021  scvxcvx  27038  lgamgulmlem5  27085  lgambdd  27089  lgamcvglem  27092  wilthlem2  27121  fsumdvdscom  27237  musumsum  27244  chtub  27264  fsumvma  27265  perfectlem2  27282  dchrelbas3  27290  dchrelbasd  27291  dchrn0  27302  dchrptlem2  27317  lgsval2lem  27359  lgsdirnn0  27396  lgsdinn0  27397  2sqlem10  27480  dchrisumlem1  27541  dchrmusum2  27546  dchrvmasumlem2  27550  dchrvmasumlem3  27551  dchrvmasumiflem1  27553  dchrisum0flblem2  27561  dchrisum0flb  27562  dchrisum0lem1b  27567  dchrisum0lem2  27570  2vmadivsumlem  27592  chpdifbndlem1  27605  selberg3lem1  27609  selberg4lem1  27612  pntrsumbnd2  27619  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem5  27633  pntrlog2bndlem6  27635  pntibndlem2  27643  pntibndlem3  27644  pntlemn  27652  pntlemj  27655  pntlemi  27656  pntlemo  27659  pntleme  27660  pntlem3  27661  pntlemp  27662  ostth2lem1  27670  ostthlem1  27679  ostth2lem2  27686  ostth3  27690  nosupprefixmo  27752  noinfprefixmo  27753  noinfbnd1lem1  27775  noinfbnd1lem4  27778  noinfbnd2lem1  27782  noinfbnd2  27783  eqcuts3  27885  cofslts  27999  coinitslts  28000  leadds1  28070  addsass  28086  addbdaylem  28098  negsid  28122  mulscom  28220  addsdilem3  28234  addsdilem4  28235  mulsasslem3  28246  precsexlem8  28295  precsexlem9  28296  precsexlem11  28298  addonbday  28360  n0fincut  28436  onsfi  28437  bdayfinbndlem1  28548  bdayfinbnd  28550  tglowdim1i  28658  tglowdim2ln  28808  wlkonl1iedg  29821  wlkp1lem7  29835  wlkp1lem8  29836  crctcshwlkn0lem6  29972  eupth2eucrct  30376  eupth2lem3  30395  ubthlem1  31030  ubthlem2  31031  minvecolem3  31036  occllem  31463  pjhthlem1  31551  eqelbid  32633  fnfvor  32772  ofrco  32773  wrdt2ind  33092  mgccole1  33129  mgcmnt2  33132  dfmgc2  33135  fxpgaeq  33310  fxpsubm  33313  fxpsubg  33314  fxpsubrg  33315  elrgspnlem4  33387  elrgspnsubrunlem2  33390  0nellinds  33517  linds2eq  33528  elrspunidl  33575  prmidl  33587  mxidlmax  33614  ssmxidl  33623  1arithidomlem1  33692  1arithidom  33694  1arithufdlem3  33703  1arithufdlem4  33704  ply1dg1rt  33737  vietalem  33837  lbsdiflsp0  33884  fedgmullem1  33887  fedgmullem2  33888  extdg1id  33924  fldextrspunlsplem  33931  extdgfialglem2  33951  constrsscn  33998  constrconj  34003  zrhcntr  34237  ofcfeqd2  34359  inelpisys  34412  unelldsys  34416  ldgenpisyslem1  34421  mbfmcnvima  34513  signstfvneq0  34827  fsum2dsub  34862  hgt750lemc  34902  hgt750lemd  34903  hgt749d  34904  hgt750lemf  34908  bnj1379  35086  bnj1450  35306  revwlk  35436  subfacp1lem5  35495  cvmlift2lem10  35623  nmulprop  36501  nmulcom  36505  weiunfrlem  36785  weiunpo  36786  weiunso  36787  weiunfr  36788  weiunse  36789  unblimceq0lem  36905  unblimceq0  36906  unbdqndv2  36910  bj-ismoored  37558  lcmineqlem4  42610  dvle2  42650  aks4d1p9  42666  primrootlekpowne0  42683  aks6d1c1p3  42688  aks6d1c1p4  42689  aks6d1c1p5  42690  aks6d1c1  42694  hashscontpow  42700  aks6d1c2lem3  42704  sticksstones1  42724  aks6d1c6lem1  42748  aks6d1c6lem2  42749  aks6d1c6lem4  42751  aks6d1c7  42762  aks5lem3a  42767  unitscyglem1  42773  unitscyglem2  42774  unitscyglem3  42775  unitscyglem4  42776  exfinfldd  42781  fnwe2lem2  43589  aomclem4  43595  scottelrankd  44784  mnuop123d  44799  mnuprdlem1  44809  mnuprdlem2  44810  eliind  45612  rnmptbd2lem  45784  rnmptbdlem  45791  cvgcau  46025  limclner  46186  climisp  46281  climrescn  46283  climxrrelem  46284  climxrre  46285  liminflelimsuplem  46310  cncfshift  46409  cncfperiod  46414  fperdvper  46454  fourierdlem48  46689  salunicl  46851  saldifcl  46854  meadjuni  46992  chnerlem1  47419  lubsscl  49542  glbsscl  49543  ipolub  49570  ipoglb  49573  ssccatid  49654  upciclem1  49748  oppcup3lem  49788  oppcthinendcALT  50023  setcthin  50047