Theorem rspcdva 3580

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045

This theorem is referenced by:  nvocnv  7222  knatar  7298  caofref  7648  caofinvl  7649  tfisi  7799  frxp2  8084  frxp3  8091  suppssov1  8137  suppssov2  8138  fpr3g  8225  fprresex  8250  tfrlem1  8305  tfrlem5  8309  coflton  8596  cofon1  8597  cofon2  8598  marypha1lem  9342  marypha1  9343  ordtypelem6  9434  ordtypelem7  9435  wemaplem2  9458  oemapvali  9599  cantnflem1c  9602  ttrcltr  9631  ttrclss  9635  dmttrcl  9636  rnttrcl  9637  ttrclselem2  9641  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  10560  pwfseqlem5  10576  winalim2  10609  wununi  10619  wunpw  10620  dedekind  11297  zsupss  12856  uzwo3  12862  seqcl2  13945  seqcl  13947  seqf  13948  seqfveq2  13949  seqfveq  13951  seqshft2  13953  monoord  13957  monoord2  13958  sermono  13959  seqsplit  13960  seqcaopr3  13962  seqid  13972  seqid2  13973  seqhomo  13974  seqz  13975  discr1  14164  discr  14165  hashbclem  14377  wrdind  14646  limsupgre  15406  climi  15435  rlimi  15438  rlimclim1  15470  rlimclim  15471  climrlim2  15472  rlimcn1  15513  climcn1  15517  isercoll2  15594  caucvgrlem  15598  caucvgb  15605  iseraltlem2  15608  iseraltlem3  15609  fsumm1  15676  fsum1p  15678  fsumcom2  15699  fsumge1  15722  telfsumo  15727  telfsumo2  15728  fsumparts  15731  o1fsum  15738  isum1p  15766  isumnn0nn  15767  isumrpcl  15768  climcndslem1  15774  climcndslem2  15775  climcnds  15776  cvgrat  15808  mertenslem1  15809  mertens  15811  fprodm1  15892  fprod1p  15893  fprodcom2  15909  prmind2  16614  pcmpt2  16823  prmpwdvds  16834  prmreclem4  16849  prmreclem5  16850  vdwlem1  16911  vdwlem2  16912  vdwlem9  16919  vdwlem10  16920  rami  16945  ramcl  16959  prmodvdslcmf  16977  prmgaplcmlem1  16981  cshwsidrepsw  17023  prdsbasprj  17394  isacs2  17577  acsfiel  17578  catidex  17598  iscatd2  17605  catlid  17607  catrid  17608  subcidcl  17769  funcid  17795  yonedalem4c  18201  yonffthlem  18206  isdrs2  18230  luble  18281  glble  18294  joinle  18308  meetle  18322  poslubmo  18333  posglbmo  18334  acsdrsel  18467  isacs4lem  18468  isacs5lem  18469  acsdrscl  18470  acsficl  18471  lidrideqd  18561  grpinvalem  18565  grpinva  18566  mndind  18720  grpidd2  18874  mulgsubcl  18985  issubg4  19042  ghmf1  19143  fislw  19522  efgsdmi  19629  efgsrel  19631  gexexlem  19749  gsumzaddlem  19818  gsummhm2  19836  dprdcntz  19907  dprddisj  19908  dprdss  19928  dprd2dlem2  19939  dprd2da  19941  dpjrid  19961  ablfac1eu  19972  pgpfac1lem1  19973  pgpfaclem2  19981  lringuplu  20447  issrngd  20758  islbs2  21079  lbsextlem4  21086  prmirredlem  21397  psgndiflemB  21525  frlmphl  21706  mplsubglem  21924  mpllsslem  21925  subrgasclcl  21990  mplind  21993  evlslem1  22005  ply1scleq  22208  mdetralt  22511  mdetunilem1  22515  lmcvg  23165  iscncl  23172  lmff  23204  cnrmi  23263  cmpcov  23292  fiuncmp  23307  hauscmplem  23309  1stcfb  23348  1stcelcls  23364  restnlly  23385  islly2  23387  lly1stc  23399  kgeni  23440  ptpjpre1  23474  ptbasfi  23484  ptpjopn  23515  dfac14  23521  txtube  23543  cnmpt11  23566  cnmpt21  23574  cnmptkp  23583  cnmptk1p  23588  qtopomap  23621  qtopcmap  23622  flimcf  23885  fclscf  23928  flfcntr  23946  ptcmplem3  23957  tgpt0  24022  tsmsi  24037  tsmsxplem2  24057  tsmsxp  24058  isucn2  24182  ucnima  24184  ucncn  24188  cfiluweak  24198  cuspcvg  24204  imasdsf1olem  24277  lpbl  24407  comet  24417  cfilucfil  24463  cnheiborlem  24869  cnheibor  24870  bndth  24873  nmoleub2lem2  25032  nmoleub3  25035  ipcau2  25150  tcphcphlem1  25151  tcphcphlem2  25152  lmmcvg  25177  cmetcaulem  25204  iscmet3lem1  25207  iscmet3lem2  25208  pjthlem1  25353  pjthlem2  25354  ivthlem1  25368  ivthlem2  25369  ivthlem3  25370  ivth2  25372  ivthle  25373  ivthle2  25374  ivthicc  25375  ovoliunlem1  25419  ovolshftlem1  25426  ovolscalem1  25430  ovolicc2lem3  25436  ovolicc2lem4  25437  ovolicc2  25439  volsup  25473  dyadmbl  25517  vitalilem2  25526  vitalilem3  25527  mbfdm  25543  ismbf3d  25571  cncombf  25575  itg2seq  25659  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  iblitg  25685  itgconst  25736  itgfsum  25744  limcvallem  25788  cnlimci  25806  cnmptlimc  25807  dvferm1lem  25904  dvferm1  25905  dvferm2lem  25906  dvferm2  25907  dvlipcn  25915  dvle  25928  lhop1lem  25934  dvfsumge  25944  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  ftc1a  25960  ftc1lem4  25962  itgsubstlem  25971  mdeglt  25986  deg1lt  26018  ply1divex  26058  fta1glem2  26090  fta1g  26091  plyco0  26113  plyeq0lem  26131  dgrcolem2  26196  plydivlem4  26220  plydivex  26221  fta1lem  26231  vieta1lem2  26235  vieta1  26236  tayl0  26285  ulmi  26311  ulmdvlem1  26325  ulmdvlem3  26327  ulmdv  26328  mtest  26329  pserulm  26347  efif1olem4  26470  rlimcnp  26891  rlimcnp2  26892  xrlimcnp  26894  scvxcvx  26912  lgamgulmlem5  26959  lgambdd  26963  lgamcvglem  26966  wilthlem2  26995  fsumdvdscom  27111  musumsum  27118  chtub  27139  fsumvma  27140  perfectlem2  27157  dchrelbas3  27165  dchrelbasd  27166  dchrn0  27177  dchrptlem2  27192  lgsval2lem  27234  lgsdirnn0  27271  lgsdinn0  27272  2sqlem10  27355  dchrisumlem1  27416  dchrmusum2  27421  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrisum0flblem2  27436  dchrisum0flb  27437  dchrisum0lem1b  27442  dchrisum0lem2  27445  2vmadivsumlem  27467  chpdifbndlem1  27480  selberg3lem1  27484  selberg4lem1  27487  pntrsumbnd2  27494  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntibndlem2  27518  pntibndlem3  27519  pntlemn  27527  pntlemj  27530  pntlemi  27531  pntlemo  27534  pntleme  27535  pntlem3  27536  pntlemp  27537  ostth2lem1  27545  ostthlem1  27554  ostth2lem2  27561  ostth3  27565  nosupprefixmo  27628  noinfprefixmo  27629  noinfbnd1lem1  27651  noinfbnd1lem4  27654  noinfbnd2lem1  27658  noinfbnd2  27659  eqscut3  27753  cofsslt  27849  coinitsslt  27850  sleadd1  27919  addsass  27935  addsbdaylem  27946  negsid  27970  mulscom  28065  addsdilem3  28079  addsdilem4  28080  mulsasslem3  28091  precsexlem8  28139  precsexlem9  28140  precsexlem11  28142  n0sfincut  28269  onsfi  28270  zs12bday  28379  tglowdim1i  28464  tglowdim2ln  28614  wlkonl1iedg  29627  wlkp1lem7  29641  wlkp1lem8  29642  crctcshwlkn0lem6  29778  eupth2eucrct  30179  eupth2lem3  30198  ubthlem1  30832  ubthlem2  30833  minvecolem3  30838  occllem  31265  pjhthlem1  31353  eqelbid  32437  wrdt2ind  32908  mgccole1  32945  mgcmnt2  32948  dfmgc2  32951  chnltm1  32963  chnub  32967  fxpgaeq  33124  fxpsubm  33127  fxpsubg  33128  fxpsubrg  33129  elrgspnlem4  33198  elrgspnsubrunlem2  33201  0nellinds  33320  linds2eq  33331  elrspunidl  33378  prmidl  33390  mxidlmax  33415  ssmxidl  33424  1arithidomlem1  33485  1arithidom  33487  1arithufdlem3  33496  1arithufdlem4  33497  ply1dg1rt  33527  lbsdiflsp0  33601  fedgmullem1  33604  fedgmullem2  33605  extdg1id  33640  fldextrspunlsplem  33647  constrsscn  33709  constrconj  33714  zrhcntr  33948  ofcfeqd2  34070  inelpisys  34123  unelldsys  34127  ldgenpisyslem1  34132  mbfmcnvima  34225  signstfvneq0  34542  fsum2dsub  34577  hgt750lemc  34617  hgt750lemd  34618  hgt749d  34619  hgt750lemf  34623  bnj1379  34799  bnj1450  35019  revwlk  35100  subfacp1lem5  35159  cvmlift2lem10  35287  weiunfrlem  36440  weiunpo  36441  weiunso  36442  weiunfr  36443  weiunse  36444  unblimceq0lem  36482  unblimceq0  36483  unbdqndv2  36487  bj-ismoored  37083  lcmineqlem4  42008  dvle2  42048  aks4d1p9  42064  primrootlekpowne0  42081  aks6d1c1p3  42086  aks6d1c1p4  42087  aks6d1c1p5  42088  aks6d1c1  42092  hashscontpow  42098  aks6d1c2lem3  42102  sticksstones1  42122  aks6d1c6lem1  42146  aks6d1c6lem2  42147  aks6d1c6lem4  42149  aks6d1c7  42160  aks5lem3a  42165  unitscyglem1  42171  unitscyglem2  42172  unitscyglem3  42173  unitscyglem4  42174  exfinfldd  42179  fnwe2lem2  43027  aomclem4  43033  scottelrankd  44223  mnuop123d  44238  mnuprdlem1  44248  mnuprdlem2  44249  eliind  45052  rnmptbd2lem  45229  rnmptbdlem  45236  cvgcau  45473  limclner  45636  climisp  45731  climrescn  45733  climxrrelem  45734  climxrre  45735  liminflelimsuplem  45760  cncfshift  45859  cncfperiod  45864  fperdvper  45904  salunicl  46301  saldifcl  46304  meadjuni  46442  lubsscl  48948  glbsscl  48949  ipolub  48976  ipoglb  48979  ssccatid  49061  upciclem1  49155  oppcup3lem  49195  oppcthinendcALT  49430  setcthin  49454