Theorem rspcdva 3577

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 3572	. 2 ⊢ (𝐶 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝜓 → 𝜒))
5	1, 2, 4	sylc 66	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∀wral 3076

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-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077

This theorem is used by:  nvocnv  7282  knatar  7360  caofref  7709  caofinvl  7710  tfisi  7855  frxp2  8142  frxp3  8149  suppssov1  8195  suppssov2  8196  fpr3g  8284  fprresex  8309  tfrlem1  8364  tfrlem5  8368  coflton  8659  cofon1  8660  cofon2  8661  marypha1lem  9403  marypha1  9404  ordtypelem6  9495  ordtypelem7  9496  wemaplem2  9519  oemapvali  9663  cantnflem1c  9666  ttrcltr  9695  ttrclss  9699  dmttrcl  9700  rnttrcl  9701  ttrclselem2  9705  scottelrankd  9887  infxpenlem  10016  acni  10048  dfac9  10139  dfac12lem2  10147  sornom  10279  fin1ai  10295  fin2i  10297  fin23lem11  10319  isfin2-2  10321  fin23lem17  10340  fin23lem39  10352  fin1a2lem13  10414  hsmexlem4  10431  ttukeylem5  10515  ttukeylem6  10516  canth4  10656  pwfseqlem5  10672  winalim2  10705  wununi  10715  wunpw  10716  dedekind  11397  zsupss  12986  uzwo3  12992  seqcl2  14084  seqcl  14086  seqf  14087  seqfveq2  14088  seqfveq  14090  seqshft2  14092  monoord  14096  monoord2  14097  sermono  14098  seqsplit  14099  seqcaopr3  14101  seqid  14111  seqid2  14112  seqhomo  14113  seqz  14114  discr1  14303  discr  14304  hashbclem  14517  wrdind  14791  limsupgre  15568  climi  15597  rlimi  15600  rlimclim1  15632  rlimclim  15633  climrlim2  15634  rlimcn1  15675  climcn1  15679  isercoll2  15756  caucvgrlem  15760  caucvgb  15767  iseraltlem2  15770  iseraltlem3  15771  fsumm1  15837  fsum1p  15839  fsumcom2  15860  fsumge1  15884  telfsumo  15889  telfsumo2  15890  fsumparts  15893  o1fsum  15900  isum1p  15930  isumnn0nn  15931  isumrpcl  15932  climcndslem1  15938  climcndslem2  15939  climcnds  15940  cvgrat  15972  mertenslem1  15973  mertens  15975  fprodm1  16054  fprod1p  16055  fprodcom2  16071  prmind2  16775  pcmpt2  16985  prmpwdvds  16996  prmreclem4  17011  prmreclem5  17012  vdwlem1  17073  vdwlem2  17074  vdwlem9  17081  vdwlem10  17082  rami  17107  ramcl  17121  prmodvdslcmf  17139  prmgaplcmlem1  17143  cshwsidrepsw  17185  prdsbasprj  17557  isacs2  17741  acsfiel  17742  catidex  17762  iscatd2  17769  catlid  17771  catrid  17772  subcidcl  17933  funcid  17959  yonedalem4c  18365  yonffthlem  18370  isdrs2  18394  luble  18445  glble  18458  joinle  18472  meetle  18486  poslubmo  18497  posglbmo  18498  acsdrsel  18631  isacs4lem  18632  isacs5lem  18633  acsdrscl  18634  acsficl  18635  chnltm1  18697  chnub  18710  lidrideqd  18763  grpinvalem  18767  grpinva  18768  mndind  18937  grpidd2  19101  mulgsubcl  19211  issubg4  19269  ghmf1  19373  fislw  19752  efgsdmi  19859  efgsrel  19861  gexexlem  19979  gsumzaddlem  20048  gsummhm2  20066  dprdcntz  20137  dprddisj  20138  dprdss  20158  dprd2dlem2  20169  dprd2da  20171  dpjrid  20191  ablfac1eu  20202  pgpfac1lem1  20203  pgpfaclem2  20211  lringuplu  20706  issrngd  21021  islbs2  21341  lbsextlem4  21348  prmidl  21528  prmirredlem  21685  psgndiflemB  21813  frlmphl  21994  mplsubglem  22213  mpllsslem  22214  subrgasclcl  22283  mplind  22286  evlslem1  22298  ply1scleq  22530  mdetralt  22830  mdetunilem1  22834  lmcvg  23487  iscncl  23494  lmff  23526  cnrmi  23585  cmpcov  23614  fiuncmp  23629  hauscmplem  23631  1stcfb  23670  1stcelcls  23687  restnlly  23708  islly2  23710  lly1stc  23722  kgeni  23763  ptpjpre1  23797  ptbasfi  23807  ptpjopn  23838  dfac14  23844  txtube  23866  cnmpt11  23889  cnmpt21  23897  cnmptkp  23906  cnmptk1p  23911  qtopomap  23944  qtopcmap  23945  flimcf  24208  fclscf  24251  flfcntr  24269  ptcmplem3  24280  tgpt0  24345  tsmsi  24360  tsmsxplem2  24380  tsmsxp  24381  isucn2  24504  ucnima  24506  ucncn  24510  cfiluweak  24520  cuspcvg  24526  imasdsf1olem  24599  lpbl  24729  comet  24739  cfilucfil  24785  cnheiborlem  25182  cnheibor  25183  bndth  25186  nmoleub2lem2  25344  nmoleub3  25347  ipcau2  25462  tcphcphlem1  25463  tcphcphlem2  25464  lmmcvg  25489  cmetcaulem  25516  iscmet3lem1  25519  iscmet3lem2  25520  pjthlem1  25665  pjthlem2  25666  ivthlem1  25679  ivthlem2  25680  ivthlem3  25681  ivth2  25683  ivthle  25684  ivthle2  25685  ivthicc  25686  ovoliunlem1  25730  ovolshftlem1  25737  ovolscalem1  25741  ovolicc2lem3  25747  ovolicc2lem4  25748  ovolicc2  25750  volsup  25784  dyadmbl  25828  vitalilem2  25837  vitalilem3  25838  mbfdm  25854  ismbf3d  25882  cncombf  25886  itg2seq  25970  itg2monolem2  25979  itg2monolem3  25980  itg2mono  25981  iblitg  25996  itgconst  26046  itgfsum  26054  limcvallem  26098  cnlimci  26116  cnmptlimc  26117  dvferm1lem  26211  dvferm1  26212  dvferm2lem  26213  dvferm2  26214  dvlipcn  26221  dvle  26234  lhop1lem  26240  dvfsumge  26249  dvfsumlem2  26254  dvfsumlem3  26255  ftc1a  26264  ftc1lem4  26266  itgsubstlem  26275  mdeglt  26290  deg1lt  26322  ply1divex  26362  fta1glem2  26394  fta1g  26395  plyco0  26417  plyeq0lem  26436  dgrcolem2  26500  plydivlem4  26526  plydivex  26527  fta1lem  26537  vieta1lem2  26543  vieta1  26544  tayl0  26598  ulmi  26622  ulmdvlem1  26636  ulmdvlem3  26638  ulmdv  26639  mtest  26640  pserulm  26658  efif1olem4  26782  rlimcnp  27202  rlimcnp2  27203  xrlimcnp  27205  scvxcvx  27222  lgamgulmlem5  27269  lgambdd  27273  lgamcvglem  27276  wilthlem2  27305  fsumdvdscom  27421  musumsum  27428  chtub  27448  fsumvma  27449  perfectlem2  27466  dchrelbas3  27474  dchrelbasd  27475  dchrn0  27486  dchrptlem2  27501  lgsval2lem  27543  lgsdirnn0  27580  lgsdinn0  27581  2sqlem10  27664  dchrisumlem1  27725  dchrmusum2  27730  dchrvmasumlem2  27734  dchrvmasumlem3  27735  dchrvmasumiflem1  27737  dchrisum0flblem2  27745  dchrisum0flb  27746  dchrisum0lem1b  27751  dchrisum0lem2  27754  2vmadivsumlem  27776  chpdifbndlem1  27789  selberg3lem1  27793  selberg4lem1  27796  pntrsumbnd2  27803  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntibndlem2  27827  pntibndlem3  27828  pntlemn  27836  pntlemj  27839  pntlemi  27840  pntlemo  27843  pntleme  27844  pntlem3  27845  pntlemp  27846  ostth2lem1  27854  ostthlem1  27863  ostth2lem2  27870  ostth3  27874  nosupprefixmo  27936  noinfprefixmo  27937  noinfbnd1lem1  27959  noinfbnd1lem4  27962  noinfbnd2lem1  27966  noinfbnd2  27967  eqcuts3  28069  cofslts  28183  coinitslts  28184  leadds1  28254  addsass  28270  addbdaylem  28282  negsid  28306  mulscom  28404  addsdilem3  28418  addsdilem4  28419  mulsasslem3  28430  precsexlem8  28479  precsexlem9  28480  precsexlem11  28482  addonbday  28544  n0fincut  28620  onsfi  28621  bdayfinbndlem1  28732  bdayfinbnd  28734  tglowdim1i  28843  tglowdim2ln  28999  wlkonl1iedg  30123  wlkp1lem7  30137  wlkp1lem8  30138  revwlk  30146  crctcshwlkn0lem6  30283  eupth2eucrct  30697  eupth2lem3  30716  ubthlem1  31351  ubthlem2  31352  minvecolem3  31357  occllem  31784  pjhthlem1  31872  eqelbid  32950  fnfvor  33082  ofrco  33083  wrdt2ind  33395  mgccole1  33430  mgcmnt2  33433  dfmgc2  33436  fxpgaeq  33609  fxpsubm  33612  fxpsubg  33613  fxpsubrg  33614  elrgspnlem4  33685  elrgspnsubrunlem2  33688  0nellinds  33805  linds2eq  33814  elrspunidl  33856  mxidlmax  33868  ssmxidl  33877  1arithidomlem1  33945  1arithidom  33947  1arithufdlem3  33956  1arithufdlem4  33957  ply1dg1rt  33990  vietalem  34089  lbsdiflsp0  34136  fedgmullem1  34139  fedgmullem2  34140  extdg1id  34176  fldextrspunlsplem  34183  extdgfialglem2  34203  constrsscn  34250  constrconj  34255  zrhcntr  34489  ofcfeqd2  34611  inelpisys  34665  unelldsys  34669  ldgenpisyslem1  34674  mbfmcnvima  34766  signstfvneq0  35080  fsum2dsub  35115  hgt750lemc  35155  hgt750lemd  35156  hgt749d  35157  hgt750lemf  35161  bnj1379  35339  bnj1450  35559  subfacp1lem5  35763  cvmlift2lem10  35891  nmulprop  36770  nmulcom  36774  nadddilem1  36800  nadddilem3  36802  weiunfrlem  37083  weiunpo  37084  weiunso  37085  weiunfr  37086  weiunse  37087  unblimceq0lem  37203  unblimceq0  37204  unbdqndv2  37208  bj-ismoored  37857  lcmineqlem4  42898  dvle2  42938  aks4d1p9  42954  primrootlekpowne0  42971  aks6d1c1p3  42976  aks6d1c1p4  42977  aks6d1c1p5  42978  aks6d1c1  42982  hashscontpow  42988  aks6d1c2lem3  42992  sticksstones1  43012  aks6d1c6lem1  43036  aks6d1c6lem2  43037  aks6d1c6lem4  43039  aks6d1c7  43050  aks5lem3a  43055  unitscyglem1  43061  unitscyglem2  43062  unitscyglem3  43063  unitscyglem4  43064  exfinfldd  43069  fnwe2lem2  43892  aomclem4  43898  mnuop123d  45086  mnuprdlem1  45096  mnuprdlem2  45097  eliind  45905  rnmptbd2lem  46077  rnmptbdlem  46084  cvgcau  46318  limclner  46479  climisp  46574  climrescn  46576  climxrrelem  46577  climxrre  46578  liminflelimsuplem  46603  cncfshift  46702  cncfperiod  46707  fperdvper  46747  fourierdlem48  46982  salunicl  47144  saldifcl  47147  meadjuni  47285  chnerlem1  47710  lubsscl  49886  glbsscl  49887  ipolub  49914  ipoglb  49917  ssccatid  49998  upciclem1  50092  oppcup3lem  50132  oppcthinendcALT  50367  setcthin  50391  veroquadmodzerod  50817