Theorem rspcdva 3576

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2110  ∀wral 3045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046

This theorem is referenced by:  nvocnv  7210  knatar  7286  caofref  7636  caofinvl  7637  tfisi  7784  frxp2  8069  frxp3  8076  suppssov1  8122  suppssov2  8123  fpr3g  8210  fprresex  8235  tfrlem1  8290  tfrlem5  8294  coflton  8581  cofon1  8582  cofon2  8583  marypha1lem  9312  marypha1  9313  ordtypelem6  9404  ordtypelem7  9405  wemaplem2  9428  oemapvali  9569  cantnflem1c  9572  ttrcltr  9601  ttrclss  9605  dmttrcl  9606  rnttrcl  9607  ttrclselem2  9611  infxpenlem  9896  acni  9928  dfac9  10020  dfac12lem2  10028  sornom  10160  fin1ai  10176  fin2i  10178  fin23lem11  10200  isfin2-2  10202  fin23lem17  10221  fin23lem39  10233  fin1a2lem13  10295  hsmexlem4  10312  ttukeylem5  10396  ttukeylem6  10397  canth4  10530  pwfseqlem5  10546  winalim2  10579  wununi  10589  wunpw  10590  dedekind  11268  zsupss  12827  uzwo3  12833  seqcl2  13919  seqcl  13921  seqf  13922  seqfveq2  13923  seqfveq  13925  seqshft2  13927  monoord  13931  monoord2  13932  sermono  13933  seqsplit  13934  seqcaopr3  13936  seqid  13946  seqid2  13947  seqhomo  13948  seqz  13949  discr1  14138  discr  14139  hashbclem  14351  wrdind  14621  limsupgre  15380  climi  15409  rlimi  15412  rlimclim1  15444  rlimclim  15445  climrlim2  15446  rlimcn1  15487  climcn1  15491  isercoll2  15568  caucvgrlem  15572  caucvgb  15579  iseraltlem2  15582  iseraltlem3  15583  fsumm1  15650  fsum1p  15652  fsumcom2  15673  fsumge1  15696  telfsumo  15701  telfsumo2  15702  fsumparts  15705  o1fsum  15712  isum1p  15740  isumnn0nn  15741  isumrpcl  15742  climcndslem1  15748  climcndslem2  15749  climcnds  15750  cvgrat  15782  mertenslem1  15783  mertens  15785  fprodm1  15866  fprod1p  15867  fprodcom2  15883  prmind2  16588  pcmpt2  16797  prmpwdvds  16808  prmreclem4  16823  prmreclem5  16824  vdwlem1  16885  vdwlem2  16886  vdwlem9  16893  vdwlem10  16894  rami  16919  ramcl  16933  prmodvdslcmf  16951  prmgaplcmlem1  16955  cshwsidrepsw  16997  prdsbasprj  17368  isacs2  17551  acsfiel  17552  catidex  17572  iscatd2  17579  catlid  17581  catrid  17582  subcidcl  17743  funcid  17769  yonedalem4c  18175  yonffthlem  18180  isdrs2  18204  luble  18255  glble  18268  joinle  18282  meetle  18296  poslubmo  18307  posglbmo  18308  acsdrsel  18441  isacs4lem  18442  isacs5lem  18443  acsdrscl  18444  acsficl  18445  chnltm1  18507  chnub  18520  lidrideqd  18569  grpinvalem  18573  grpinva  18574  mndind  18728  grpidd2  18882  mulgsubcl  18993  issubg4  19050  ghmf1  19151  fislw  19530  efgsdmi  19637  efgsrel  19639  gexexlem  19757  gsumzaddlem  19826  gsummhm2  19844  dprdcntz  19915  dprddisj  19916  dprdss  19936  dprd2dlem2  19947  dprd2da  19949  dpjrid  19969  ablfac1eu  19980  pgpfac1lem1  19981  pgpfaclem2  19989  lringuplu  20452  issrngd  20763  islbs2  21084  lbsextlem4  21091  prmirredlem  21402  psgndiflemB  21530  frlmphl  21711  mplsubglem  21929  mpllsslem  21930  subrgasclcl  21995  mplind  21998  evlslem1  22010  ply1scleq  22213  mdetralt  22516  mdetunilem1  22520  lmcvg  23170  iscncl  23177  lmff  23209  cnrmi  23268  cmpcov  23297  fiuncmp  23312  hauscmplem  23314  1stcfb  23353  1stcelcls  23369  restnlly  23390  islly2  23392  lly1stc  23404  kgeni  23445  ptpjpre1  23479  ptbasfi  23489  ptpjopn  23520  dfac14  23526  txtube  23548  cnmpt11  23571  cnmpt21  23579  cnmptkp  23588  cnmptk1p  23593  qtopomap  23626  qtopcmap  23627  flimcf  23890  fclscf  23933  flfcntr  23951  ptcmplem3  23962  tgpt0  24027  tsmsi  24042  tsmsxplem2  24062  tsmsxp  24063  isucn2  24186  ucnima  24188  ucncn  24192  cfiluweak  24202  cuspcvg  24208  imasdsf1olem  24281  lpbl  24411  comet  24421  cfilucfil  24467  cnheiborlem  24873  cnheibor  24874  bndth  24877  nmoleub2lem2  25036  nmoleub3  25039  ipcau2  25154  tcphcphlem1  25155  tcphcphlem2  25156  lmmcvg  25181  cmetcaulem  25208  iscmet3lem1  25211  iscmet3lem2  25212  pjthlem1  25357  pjthlem2  25358  ivthlem1  25372  ivthlem2  25373  ivthlem3  25374  ivth2  25376  ivthle  25377  ivthle2  25378  ivthicc  25379  ovoliunlem1  25423  ovolshftlem1  25430  ovolscalem1  25434  ovolicc2lem3  25440  ovolicc2lem4  25441  ovolicc2  25443  volsup  25477  dyadmbl  25521  vitalilem2  25530  vitalilem3  25531  mbfdm  25547  ismbf3d  25575  cncombf  25579  itg2seq  25663  itg2monolem2  25672  itg2monolem3  25673  itg2mono  25674  iblitg  25689  itgconst  25740  itgfsum  25748  limcvallem  25792  cnlimci  25810  cnmptlimc  25811  dvferm1lem  25908  dvferm1  25909  dvferm2lem  25910  dvferm2  25911  dvlipcn  25919  dvle  25932  lhop1lem  25938  dvfsumge  25948  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsumlem3  25955  ftc1a  25964  ftc1lem4  25966  itgsubstlem  25975  mdeglt  25990  deg1lt  26022  ply1divex  26062  fta1glem2  26094  fta1g  26095  plyco0  26117  plyeq0lem  26135  dgrcolem2  26200  plydivlem4  26224  plydivex  26225  fta1lem  26235  vieta1lem2  26239  vieta1  26240  tayl0  26289  ulmi  26315  ulmdvlem1  26329  ulmdvlem3  26331  ulmdv  26332  mtest  26333  pserulm  26351  efif1olem4  26474  rlimcnp  26895  rlimcnp2  26896  xrlimcnp  26898  scvxcvx  26916  lgamgulmlem5  26963  lgambdd  26967  lgamcvglem  26970  wilthlem2  26999  fsumdvdscom  27115  musumsum  27122  chtub  27143  fsumvma  27144  perfectlem2  27161  dchrelbas3  27169  dchrelbasd  27170  dchrn0  27181  dchrptlem2  27196  lgsval2lem  27238  lgsdirnn0  27275  lgsdinn0  27276  2sqlem10  27359  dchrisumlem1  27420  dchrmusum2  27425  dchrvmasumlem2  27429  dchrvmasumlem3  27430  dchrvmasumiflem1  27432  dchrisum0flblem2  27440  dchrisum0flb  27441  dchrisum0lem1b  27446  dchrisum0lem2  27449  2vmadivsumlem  27471  chpdifbndlem1  27484  selberg3lem1  27488  selberg4lem1  27491  pntrsumbnd2  27498  pntrlog2bndlem2  27509  pntrlog2bndlem3  27510  pntrlog2bndlem5  27512  pntrlog2bndlem6  27514  pntibndlem2  27522  pntibndlem3  27523  pntlemn  27531  pntlemj  27534  pntlemi  27535  pntlemo  27538  pntleme  27539  pntlem3  27540  pntlemp  27541  ostth2lem1  27549  ostthlem1  27558  ostth2lem2  27565  ostth3  27569  nosupprefixmo  27632  noinfprefixmo  27633  noinfbnd1lem1  27655  noinfbnd1lem4  27658  noinfbnd2lem1  27662  noinfbnd2  27663  eqscut3  27758  cofsslt  27855  coinitsslt  27856  sleadd1  27925  addsass  27941  addsbdaylem  27952  negsid  27976  mulscom  28071  addsdilem3  28085  addsdilem4  28086  mulsasslem3  28097  precsexlem8  28145  precsexlem9  28146  precsexlem11  28148  n0sfincut  28275  onsfi  28276  zs12bday  28387  tglowdim1i  28472  tglowdim2ln  28622  wlkonl1iedg  29635  wlkp1lem7  29649  wlkp1lem8  29650  crctcshwlkn0lem6  29786  eupth2eucrct  30187  eupth2lem3  30206  ubthlem1  30840  ubthlem2  30841  minvecolem3  30846  occllem  31273  pjhthlem1  31361  eqelbid  32444  fnfvor  32582  ofrco  32583  wrdt2ind  32924  mgccole1  32961  mgcmnt2  32964  dfmgc2  32967  fxpgaeq  33128  fxpsubm  33131  fxpsubg  33132  fxpsubrg  33133  elrgspnlem4  33202  elrgspnsubrunlem2  33205  0nellinds  33325  linds2eq  33336  elrspunidl  33383  prmidl  33395  mxidlmax  33420  ssmxidl  33429  1arithidomlem1  33490  1arithidom  33492  1arithufdlem3  33501  1arithufdlem4  33502  ply1dg1rt  33533  lbsdiflsp0  33629  fedgmullem1  33632  fedgmullem2  33633  extdg1id  33669  fldextrspunlsplem  33676  extdgfialglem2  33696  constrsscn  33743  constrconj  33748  zrhcntr  33982  ofcfeqd2  34104  inelpisys  34157  unelldsys  34161  ldgenpisyslem1  34166  mbfmcnvima  34258  signstfvneq0  34575  fsum2dsub  34610  hgt750lemc  34650  hgt750lemd  34651  hgt749d  34652  hgt750lemf  34656  bnj1379  34832  bnj1450  35052  revwlk  35137  subfacp1lem5  35196  cvmlift2lem10  35324  weiunfrlem  36477  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  unblimceq0lem  36519  unblimceq0  36520  unbdqndv2  36524  bj-ismoored  37120  lcmineqlem4  42044  dvle2  42084  aks4d1p9  42100  primrootlekpowne0  42117  aks6d1c1p3  42122  aks6d1c1p4  42123  aks6d1c1p5  42124  aks6d1c1  42128  hashscontpow  42134  aks6d1c2lem3  42138  sticksstones1  42158  aks6d1c6lem1  42182  aks6d1c6lem2  42183  aks6d1c6lem4  42185  aks6d1c7  42196  aks5lem3a  42201  unitscyglem1  42207  unitscyglem2  42208  unitscyglem3  42209  unitscyglem4  42210  exfinfldd  42215  fnwe2lem2  43063  aomclem4  43069  scottelrankd  44259  mnuop123d  44274  mnuprdlem1  44284  mnuprdlem2  44285  eliind  45087  rnmptbd2lem  45264  rnmptbdlem  45271  cvgcau  45507  limclner  45668  climisp  45763  climrescn  45765  climxrrelem  45766  climxrre  45767  liminflelimsuplem  45792  cncfshift  45891  cncfperiod  45896  fperdvper  45936  salunicl  46333  saldifcl  46336  meadjuni  46474  lubsscl  48970  glbsscl  48971  ipolub  48998  ipoglb  49001  ssccatid  49083  upciclem1  49177  oppcup3lem  49217  oppcthinendcALT  49452  setcthin  49476