Theorem rspcdva 3566

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∀wral 3052

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-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053

This theorem is referenced by:  nvocnv  7229  knatar  7305  caofref  7655  caofinvl  7656  tfisi  7803  frxp2  8087  frxp3  8094  suppssov1  8140  suppssov2  8141  fpr3g  8228  fprresex  8253  tfrlem1  8308  tfrlem5  8312  coflton  8600  cofon1  8601  cofon2  8602  marypha1lem  9339  marypha1  9340  ordtypelem6  9431  ordtypelem7  9432  wemaplem2  9455  oemapvali  9596  cantnflem1c  9599  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  infxpenlem  9926  acni  9958  dfac9  10050  dfac12lem2  10058  sornom  10190  fin1ai  10206  fin2i  10208  fin23lem11  10230  isfin2-2  10232  fin23lem17  10251  fin23lem39  10263  fin1a2lem13  10325  hsmexlem4  10342  ttukeylem5  10426  ttukeylem6  10427  canth4  10561  pwfseqlem5  10577  winalim2  10610  wununi  10620  wunpw  10621  dedekind  11300  zsupss  12878  uzwo3  12884  seqcl2  13973  seqcl  13975  seqf  13976  seqfveq2  13977  seqfveq  13979  seqshft2  13981  monoord  13985  monoord2  13986  sermono  13987  seqsplit  13988  seqcaopr3  13990  seqid  14000  seqid2  14001  seqhomo  14002  seqz  14003  discr1  14192  discr  14193  hashbclem  14405  wrdind  14675  limsupgre  15434  climi  15463  rlimi  15466  rlimclim1  15498  rlimclim  15499  climrlim2  15500  rlimcn1  15541  climcn1  15545  isercoll2  15622  caucvgrlem  15626  caucvgb  15633  iseraltlem2  15636  iseraltlem3  15637  fsumm1  15704  fsum1p  15706  fsumcom2  15727  fsumge1  15751  telfsumo  15756  telfsumo2  15757  fsumparts  15760  o1fsum  15767  isum1p  15797  isumnn0nn  15798  isumrpcl  15799  climcndslem1  15805  climcndslem2  15806  climcnds  15807  cvgrat  15839  mertenslem1  15840  mertens  15842  fprodm1  15923  fprod1p  15924  fprodcom2  15940  prmind2  16645  pcmpt2  16855  prmpwdvds  16866  prmreclem4  16881  prmreclem5  16882  vdwlem1  16943  vdwlem2  16944  vdwlem9  16951  vdwlem10  16952  rami  16977  ramcl  16991  prmodvdslcmf  17009  prmgaplcmlem1  17013  cshwsidrepsw  17055  prdsbasprj  17426  isacs2  17610  acsfiel  17611  catidex  17631  iscatd2  17638  catlid  17640  catrid  17641  subcidcl  17802  funcid  17828  yonedalem4c  18234  yonffthlem  18239  isdrs2  18263  luble  18314  glble  18327  joinle  18341  meetle  18355  poslubmo  18366  posglbmo  18367  acsdrsel  18500  isacs4lem  18501  isacs5lem  18502  acsdrscl  18503  acsficl  18504  chnltm1  18566  chnub  18579  lidrideqd  18628  grpinvalem  18632  grpinva  18633  mndind  18787  grpidd2  18944  mulgsubcl  19055  issubg4  19112  ghmf1  19212  fislw  19591  efgsdmi  19698  efgsrel  19700  gexexlem  19818  gsumzaddlem  19887  gsummhm2  19905  dprdcntz  19976  dprddisj  19977  dprdss  19997  dprd2dlem2  20008  dprd2da  20010  dpjrid  20030  ablfac1eu  20041  pgpfac1lem1  20042  pgpfaclem2  20050  lringuplu  20512  issrngd  20823  islbs2  21144  lbsextlem4  21151  prmirredlem  21462  psgndiflemB  21590  frlmphl  21771  mplsubglem  21987  mpllsslem  21988  subrgasclcl  22055  mplind  22058  evlslem1  22070  ply1scleq  22280  mdetralt  22583  mdetunilem1  22587  lmcvg  23237  iscncl  23244  lmff  23276  cnrmi  23335  cmpcov  23364  fiuncmp  23379  hauscmplem  23381  1stcfb  23420  1stcelcls  23436  restnlly  23457  islly2  23459  lly1stc  23471  kgeni  23512  ptpjpre1  23546  ptbasfi  23556  ptpjopn  23587  dfac14  23593  txtube  23615  cnmpt11  23638  cnmpt21  23646  cnmptkp  23655  cnmptk1p  23660  qtopomap  23693  qtopcmap  23694  flimcf  23957  fclscf  24000  flfcntr  24018  ptcmplem3  24029  tgpt0  24094  tsmsi  24109  tsmsxplem2  24129  tsmsxp  24130  isucn2  24253  ucnima  24255  ucncn  24259  cfiluweak  24269  cuspcvg  24275  imasdsf1olem  24348  lpbl  24478  comet  24488  cfilucfil  24534  cnheiborlem  24931  cnheibor  24932  bndth  24935  nmoleub2lem2  25093  nmoleub3  25096  ipcau2  25211  tcphcphlem1  25212  tcphcphlem2  25213  lmmcvg  25238  cmetcaulem  25265  iscmet3lem1  25268  iscmet3lem2  25269  pjthlem1  25414  pjthlem2  25415  ivthlem1  25428  ivthlem2  25429  ivthlem3  25430  ivth2  25432  ivthle  25433  ivthle2  25434  ivthicc  25435  ovoliunlem1  25479  ovolshftlem1  25486  ovolscalem1  25490  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2  25499  volsup  25533  dyadmbl  25577  vitalilem2  25586  vitalilem3  25587  mbfdm  25603  ismbf3d  25631  cncombf  25635  itg2seq  25719  itg2monolem2  25728  itg2monolem3  25729  itg2mono  25730  iblitg  25745  itgconst  25796  itgfsum  25804  limcvallem  25848  cnlimci  25866  cnmptlimc  25867  dvferm1lem  25961  dvferm1  25962  dvferm2lem  25963  dvferm2  25964  dvlipcn  25971  dvle  25984  lhop1lem  25990  dvfsumge  25999  dvfsumlem2  26004  dvfsumlem3  26005  ftc1a  26014  ftc1lem4  26016  itgsubstlem  26025  mdeglt  26040  deg1lt  26072  ply1divex  26112  fta1glem2  26144  fta1g  26145  plyco0  26167  plyeq0lem  26185  dgrcolem2  26249  plydivlem4  26273  plydivex  26274  fta1lem  26284  vieta1lem2  26288  vieta1  26289  tayl0  26338  ulmi  26364  ulmdvlem1  26378  ulmdvlem3  26380  ulmdv  26381  mtest  26382  pserulm  26400  efif1olem4  26522  rlimcnp  26942  rlimcnp2  26943  xrlimcnp  26945  scvxcvx  26963  lgamgulmlem5  27010  lgambdd  27014  lgamcvglem  27017  wilthlem2  27046  fsumdvdscom  27162  musumsum  27169  chtub  27189  fsumvma  27190  perfectlem2  27207  dchrelbas3  27215  dchrelbasd  27216  dchrn0  27227  dchrptlem2  27242  lgsval2lem  27284  lgsdirnn0  27321  lgsdinn0  27322  2sqlem10  27405  dchrisumlem1  27466  dchrmusum2  27471  dchrvmasumlem2  27475  dchrvmasumlem3  27476  dchrvmasumiflem1  27478  dchrisum0flblem2  27486  dchrisum0flb  27487  dchrisum0lem1b  27492  dchrisum0lem2  27495  2vmadivsumlem  27517  chpdifbndlem1  27530  selberg3lem1  27534  selberg4lem1  27537  pntrsumbnd2  27544  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntibndlem2  27568  pntibndlem3  27569  pntlemn  27577  pntlemj  27580  pntlemi  27581  pntlemo  27584  pntleme  27585  pntlem3  27586  pntlemp  27587  ostth2lem1  27595  ostthlem1  27604  ostth2lem2  27611  ostth3  27615  nosupprefixmo  27678  noinfprefixmo  27679  noinfbnd1lem1  27701  noinfbnd1lem4  27704  noinfbnd2lem1  27708  noinfbnd2  27709  eqcuts3  27810  cofslts  27924  coinitslts  27925  leadds1  27995  addsass  28011  addbdaylem  28023  negsid  28047  mulscom  28145  addsdilem3  28159  addsdilem4  28160  mulsasslem3  28171  precsexlem8  28220  precsexlem9  28221  precsexlem11  28223  addonbday  28285  n0fincut  28361  onsfi  28362  bdayfinbndlem1  28473  bdayfinbnd  28475  tglowdim1i  28583  tglowdim2ln  28733  wlkonl1iedg  29747  wlkp1lem7  29761  wlkp1lem8  29762  crctcshwlkn0lem6  29898  eupth2eucrct  30302  eupth2lem3  30321  ubthlem1  30956  ubthlem2  30957  minvecolem3  30962  occllem  31389  pjhthlem1  31477  eqelbid  32559  fnfvor  32697  ofrco  32698  wrdt2ind  33028  mgccole1  33065  mgcmnt2  33068  dfmgc2  33071  fxpgaeq  33245  fxpsubm  33248  fxpsubg  33249  fxpsubrg  33250  elrgspnlem4  33321  elrgspnsubrunlem2  33324  0nellinds  33445  linds2eq  33456  elrspunidl  33503  prmidl  33515  mxidlmax  33540  ssmxidl  33549  1arithidomlem1  33610  1arithidom  33612  1arithufdlem3  33621  1arithufdlem4  33622  ply1dg1rt  33655  vietalem  33738  lbsdiflsp0  33786  fedgmullem1  33789  fedgmullem2  33790  extdg1id  33826  fldextrspunlsplem  33833  extdgfialglem2  33853  constrsscn  33900  constrconj  33905  zrhcntr  34139  ofcfeqd2  34261  inelpisys  34314  unelldsys  34318  ldgenpisyslem1  34323  mbfmcnvima  34415  signstfvneq0  34732  fsum2dsub  34767  hgt750lemc  34807  hgt750lemd  34808  hgt749d  34809  hgt750lemf  34813  bnj1379  34988  bnj1450  35208  revwlk  35323  subfacp1lem5  35382  cvmlift2lem10  35510  weiunfrlem  36662  weiunpo  36663  weiunso  36664  weiunfr  36665  weiunse  36666  unblimceq0lem  36782  unblimceq0  36783  unbdqndv2  36787  bj-ismoored  37435  lcmineqlem4  42485  dvle2  42525  aks4d1p9  42541  primrootlekpowne0  42558  aks6d1c1p3  42563  aks6d1c1p4  42564  aks6d1c1p5  42565  aks6d1c1  42569  hashscontpow  42575  aks6d1c2lem3  42579  sticksstones1  42599  aks6d1c6lem1  42623  aks6d1c6lem2  42624  aks6d1c6lem4  42626  aks6d1c7  42637  aks5lem3a  42642  unitscyglem1  42648  unitscyglem2  42649  unitscyglem3  42650  unitscyglem4  42651  exfinfldd  42656  fnwe2lem2  43497  aomclem4  43503  scottelrankd  44692  mnuop123d  44707  mnuprdlem1  44717  mnuprdlem2  44718  eliind  45520  rnmptbd2lem  45695  rnmptbdlem  45702  cvgcau  45936  limclner  46097  climisp  46192  climrescn  46194  climxrrelem  46195  climxrre  46196  liminflelimsuplem  46221  cncfshift  46320  cncfperiod  46325  fperdvper  46365  salunicl  46762  saldifcl  46765  meadjuni  46903  chnerlem1  47328  lubsscl  49447  glbsscl  49448  ipolub  49475  ipoglb  49478  ssccatid  49559  upciclem1  49653  oppcup3lem  49693  oppcthinendcALT  49928  setcthin  49952