Theorem rspcdva 3607

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   ∈ wcel 2107  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051

This theorem is referenced by:  nvocnv  7284  knatar  7360  caofref  7711  caofinvl  7712  tfisi  7863  frxp2  8152  frxp3  8159  suppssov1  8205  suppssov2  8206  fpr3g  8293  fprresex  8318  wfrlem17OLD  8348  tfrlem1  8399  tfrlem5  8403  coflton  8692  cofon1  8693  cofon2  8694  marypha1lem  9456  marypha1  9457  ordtypelem6  9546  ordtypelem7  9547  wemaplem2  9570  oemapvali  9707  cantnflem1c  9710  ttrcltr  9739  ttrclss  9743  dmttrcl  9744  rnttrcl  9745  ttrclselem2  9749  infxpenlem  10036  acni  10068  dfac9  10160  dfac12lem2  10168  sornom  10300  fin1ai  10316  fin2i  10318  fin23lem11  10340  isfin2-2  10342  fin23lem17  10361  fin23lem39  10373  fin1a2lem13  10435  hsmexlem4  10452  ttukeylem5  10536  ttukeylem6  10537  canth4  10670  pwfseqlem5  10686  winalim2  10719  wununi  10729  wunpw  10730  dedekind  11407  zsupss  12962  uzwo3  12968  seqcl2  14044  seqcl  14046  seqf  14047  seqfveq2  14048  seqfveq  14050  seqshft2  14052  monoord  14056  monoord2  14057  sermono  14058  seqsplit  14059  seqcaopr3  14061  seqid  14071  seqid2  14072  seqhomo  14073  seqz  14074  discr1  14261  discr  14262  hashbclem  14474  wrdind  14743  limsupgre  15500  climi  15529  rlimi  15532  rlimclim1  15564  rlimclim  15565  climrlim2  15566  rlimcn1  15607  climcn1  15611  isercoll2  15688  caucvgrlem  15692  caucvgb  15699  iseraltlem2  15702  iseraltlem3  15703  fsumm1  15770  fsum1p  15772  fsumcom2  15793  fsumge1  15816  telfsumo  15821  telfsumo2  15822  fsumparts  15825  o1fsum  15832  isum1p  15860  isumnn0nn  15861  isumrpcl  15862  climcndslem1  15868  climcndslem2  15869  climcnds  15870  cvgrat  15902  mertenslem1  15903  mertens  15905  fprodm1  15986  fprod1p  15987  fprodcom2  16003  prmind2  16705  pcmpt2  16914  prmpwdvds  16925  prmreclem4  16940  prmreclem5  16941  vdwlem1  17002  vdwlem2  17003  vdwlem9  17010  vdwlem10  17011  rami  17036  ramcl  17050  prmodvdslcmf  17068  prmgaplcmlem1  17072  cshwsidrepsw  17114  prdsbasprj  17493  isacs2  17672  acsfiel  17673  catidex  17693  iscatd2  17700  catlid  17702  catrid  17703  subcidcl  17865  funcid  17891  yonedalem4c  18297  yonffthlem  18302  isdrs2  18327  luble  18378  glble  18391  joinle  18405  meetle  18419  poslubmo  18430  posglbmo  18431  acsdrsel  18562  isacs4lem  18563  isacs5lem  18564  acsdrscl  18565  acsficl  18566  lidrideqd  18656  grpinvalem  18660  grpinva  18661  mndind  18815  grpidd2  18969  mulgsubcl  19080  issubg4  19137  ghmf1  19238  fislw  19616  efgsdmi  19723  efgsrel  19725  gexexlem  19843  gsumzaddlem  19912  gsummhm2  19930  dprdcntz  20001  dprddisj  20002  dprdss  20022  dprd2dlem2  20033  dprd2da  20035  dpjrid  20055  ablfac1eu  20066  pgpfac1lem1  20067  pgpfaclem2  20075  lringuplu  20517  issrngd  20829  islbs2  21129  lbsextlem4  21136  prmirredlem  21450  psgndiflemB  21585  frlmphl  21768  mplsubglem  21986  mpllsslem  21987  subrgasclcl  22058  mplind  22061  evlslem1  22073  ply1scleq  22276  mdetralt  22581  mdetunilem1  22585  lmcvg  23235  iscncl  23242  lmff  23274  cnrmi  23333  cmpcov  23362  fiuncmp  23377  hauscmplem  23379  1stcfb  23418  1stcelcls  23434  restnlly  23455  islly2  23457  lly1stc  23469  kgeni  23510  ptpjpre1  23544  ptbasfi  23554  ptpjopn  23585  dfac14  23591  txtube  23613  cnmpt11  23636  cnmpt21  23644  cnmptkp  23653  cnmptk1p  23658  qtopomap  23691  qtopcmap  23692  flimcf  23955  fclscf  23998  flfcntr  24016  ptcmplem3  24027  tgpt0  24092  tsmsi  24107  tsmsxplem2  24127  tsmsxp  24128  isucn2  24252  ucnima  24254  ucncn  24258  cfiluweak  24268  cuspcvg  24274  imasdsf1olem  24347  lpbl  24479  comet  24489  cfilucfil  24535  cnheiborlem  24941  cnheibor  24942  bndth  24945  nmoleub2lem2  25104  nmoleub3  25107  ipcau2  25223  tcphcphlem1  25224  tcphcphlem2  25225  lmmcvg  25250  cmetcaulem  25277  iscmet3lem1  25280  iscmet3lem2  25281  pjthlem1  25426  pjthlem2  25427  ivthlem1  25441  ivthlem2  25442  ivthlem3  25443  ivth2  25445  ivthle  25446  ivthle2  25447  ivthicc  25448  ovoliunlem1  25492  ovolshftlem1  25499  ovolscalem1  25503  ovolicc2lem3  25509  ovolicc2lem4  25510  ovolicc2  25512  volsup  25546  dyadmbl  25590  vitalilem2  25599  vitalilem3  25600  mbfdm  25616  ismbf3d  25644  cncombf  25648  itg2seq  25732  itg2monolem2  25741  itg2monolem3  25742  itg2mono  25743  iblitg  25758  itgconst  25809  itgfsum  25817  limcvallem  25861  cnlimci  25879  cnmptlimc  25880  dvferm1lem  25977  dvferm1  25978  dvferm2lem  25979  dvferm2  25980  dvlipcn  25988  dvle  26001  lhop1lem  26007  dvfsumge  26017  dvfsumlem2  26022  dvfsumlem2OLD  26023  dvfsumlem3  26024  ftc1a  26033  ftc1lem4  26035  itgsubstlem  26044  mdeglt  26059  deg1lt  26091  ply1divex  26131  fta1glem2  26163  fta1g  26164  plyco0  26186  plyeq0lem  26204  dgrcolem2  26269  plydivlem4  26293  plydivex  26294  fta1lem  26304  vieta1lem2  26308  vieta1  26309  tayl0  26358  ulmi  26384  ulmdvlem1  26398  ulmdvlem3  26400  ulmdv  26401  mtest  26402  pserulm  26420  efif1olem4  26542  rlimcnp  26963  rlimcnp2  26964  xrlimcnp  26966  scvxcvx  26984  lgamgulmlem5  27031  lgambdd  27035  lgamcvglem  27038  wilthlem2  27067  fsumdvdscom  27183  musumsum  27190  chtub  27211  fsumvma  27212  perfectlem2  27229  dchrelbas3  27237  dchrelbasd  27238  dchrn0  27249  dchrptlem2  27264  lgsval2lem  27306  lgsdirnn0  27343  lgsdinn0  27344  2sqlem10  27427  dchrisumlem1  27488  dchrmusum2  27493  dchrvmasumlem2  27497  dchrvmasumlem3  27498  dchrvmasumiflem1  27500  dchrisum0flblem2  27508  dchrisum0flb  27509  dchrisum0lem1b  27514  dchrisum0lem2  27517  2vmadivsumlem  27539  chpdifbndlem1  27552  selberg3lem1  27556  selberg4lem1  27559  pntrsumbnd2  27566  pntrlog2bndlem2  27577  pntrlog2bndlem3  27578  pntrlog2bndlem5  27580  pntrlog2bndlem6  27582  pntibndlem2  27590  pntibndlem3  27591  pntlemn  27599  pntlemj  27602  pntlemi  27603  pntlemo  27606  pntleme  27607  pntlem3  27608  pntlemp  27609  ostth2lem1  27617  ostthlem1  27626  ostth2lem2  27633  ostth3  27637  nosupprefixmo  27700  noinfprefixmo  27701  noinfbnd1lem1  27723  noinfbnd1lem4  27726  noinfbnd2lem1  27730  noinfbnd2  27731  cofsslt  27907  coinitsslt  27908  sleadd1  27977  addsass  27993  addsbdaylem  28004  negsid  28028  mulscom  28120  addsdilem3  28134  addsdilem4  28135  mulsasslem3  28146  precsexlem8  28193  precsexlem9  28194  precsexlem11  28196  zs12bday  28379  tglowdim1i  28464  tglowdim2ln  28614  wlkonl1iedg  29630  wlkp1lem7  29644  wlkp1lem8  29645  crctcshwlkn0lem6  29782  eupth2eucrct  30183  eupth2lem3  30202  ubthlem1  30836  ubthlem2  30837  minvecolem3  30842  occllem  31269  pjhthlem1  31357  eqelbid  32441  wrdt2ind  32885  mgccole1  32926  mgcmnt2  32929  dfmgc2  32932  chnltm1  32944  chnub  32948  elrgspnlem4  33195  elrgspnsubrunlem2  33198  0nellinds  33339  linds2eq  33350  elrspunidl  33397  prmidl  33409  mxidlmax  33434  ssmxidl  33443  1arithidomlem1  33504  1arithidom  33506  1arithufdlem3  33515  1arithufdlem4  33516  ply1dg1rt  33545  lbsdiflsp0  33618  fedgmullem1  33621  fedgmullem2  33622  extdg1id  33657  fldextrspunlsplem  33664  constrsscn  33722  constrconj  33727  zrhcntr  33921  ofcfeqd2  34043  inelpisys  34096  unelldsys  34100  ldgenpisyslem1  34105  mbfmcnvima  34198  signstfvneq0  34528  fsum2dsub  34563  hgt750lemc  34603  hgt750lemd  34604  hgt749d  34605  hgt750lemf  34609  bnj1379  34785  bnj1450  35005  revwlk  35071  subfacp1lem5  35130  cvmlift2lem10  35258  weiunfrlem  36406  weiunpo  36407  weiunso  36408  weiunfr  36409  weiunse  36410  unblimceq0lem  36448  unblimceq0  36449  unbdqndv2  36453  bj-ismoored  37049  lcmineqlem4  41974  dvle2  42014  aks4d1p9  42030  primrootlekpowne0  42047  aks6d1c1p3  42052  aks6d1c1p4  42053  aks6d1c1p5  42054  aks6d1c1  42058  hashscontpow  42064  aks6d1c2lem3  42068  sticksstones1  42088  aks6d1c6lem1  42112  aks6d1c6lem2  42113  aks6d1c6lem4  42115  aks6d1c7  42126  aks5lem3a  42131  unitscyglem1  42137  unitscyglem2  42138  unitscyglem3  42139  unitscyglem4  42140  exfinfldd  42145  fnwe2lem2  43008  aomclem4  43014  scottelrankd  44211  mnuop123d  44226  mnuprdlem1  44236  mnuprdlem2  44237  eliind  45021  rnmptbd2lem  45200  rnmptbdlem  45207  cvgcau  45446  limclner  45611  climisp  45706  climrescn  45708  climxrrelem  45709  climxrre  45710  cncfshift  45834  cncfperiod  45839  fperdvper  45879  salunicl  46276  saldifcl  46279  meadjuni  46417  lubsscl  48805  glbsscl  48806  ipolub  48833  ipoglb  48836  upciclem1  48882  oppcthinendcALT  49056  setcthin  49078