Theorem rspcdva 3573

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

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

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048

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  9899  acni  9931  dfac9  10023  dfac12lem2  10031  sornom  10163  fin1ai  10179  fin2i  10181  fin23lem11  10203  isfin2-2  10205  fin23lem17  10224  fin23lem39  10236  fin1a2lem13  10298  hsmexlem4  10315  ttukeylem5  10399  ttukeylem6  10400  canth4  10533  pwfseqlem5  10549  winalim2  10582  wununi  10592  wunpw  10593  dedekind  11271  zsupss  12830  uzwo3  12836  seqcl2  13922  seqcl  13924  seqf  13925  seqfveq2  13926  seqfveq  13928  seqshft2  13930  monoord  13934  monoord2  13935  sermono  13936  seqsplit  13937  seqcaopr3  13939  seqid  13949  seqid2  13950  seqhomo  13951  seqz  13952  discr1  14141  discr  14142  hashbclem  14354  wrdind  14624  limsupgre  15383  climi  15412  rlimi  15415  rlimclim1  15447  rlimclim  15448  climrlim2  15449  rlimcn1  15490  climcn1  15494  isercoll2  15571  caucvgrlem  15575  caucvgb  15582  iseraltlem2  15585  iseraltlem3  15586  fsumm1  15653  fsum1p  15655  fsumcom2  15676  fsumge1  15699  telfsumo  15704  telfsumo2  15705  fsumparts  15708  o1fsum  15715  isum1p  15743  isumnn0nn  15744  isumrpcl  15745  climcndslem1  15751  climcndslem2  15752  climcnds  15753  cvgrat  15785  mertenslem1  15786  mertens  15788  fprodm1  15869  fprod1p  15870  fprodcom2  15886  prmind2  16591  pcmpt2  16800  prmpwdvds  16811  prmreclem4  16826  prmreclem5  16827  vdwlem1  16888  vdwlem2  16889  vdwlem9  16896  vdwlem10  16897  rami  16922  ramcl  16936  prmodvdslcmf  16954  prmgaplcmlem1  16958  cshwsidrepsw  17000  prdsbasprj  17371  isacs2  17554  acsfiel  17555  catidex  17575  iscatd2  17582  catlid  17584  catrid  17585  subcidcl  17746  funcid  17772  yonedalem4c  18178  yonffthlem  18183  isdrs2  18207  luble  18258  glble  18271  joinle  18285  meetle  18299  poslubmo  18310  posglbmo  18311  acsdrsel  18444  isacs4lem  18445  isacs5lem  18446  acsdrscl  18447  acsficl  18448  chnltm1  18510  chnub  18523  lidrideqd  18572  grpinvalem  18576  grpinva  18577  mndind  18731  grpidd2  18885  mulgsubcl  18996  issubg4  19053  ghmf1  19153  fislw  19532  efgsdmi  19639  efgsrel  19641  gexexlem  19759  gsumzaddlem  19828  gsummhm2  19846  dprdcntz  19917  dprddisj  19918  dprdss  19938  dprd2dlem2  19949  dprd2da  19951  dpjrid  19971  ablfac1eu  19982  pgpfac1lem1  19983  pgpfaclem2  19991  lringuplu  20454  issrngd  20765  islbs2  21086  lbsextlem4  21093  prmirredlem  21404  psgndiflemB  21532  frlmphl  21713  mplsubglem  21931  mpllsslem  21932  subrgasclcl  21997  mplind  22000  evlslem1  22012  ply1scleq  22215  mdetralt  22518  mdetunilem1  22522  lmcvg  23172  iscncl  23179  lmff  23211  cnrmi  23270  cmpcov  23299  fiuncmp  23314  hauscmplem  23316  1stcfb  23355  1stcelcls  23371  restnlly  23392  islly2  23394  lly1stc  23406  kgeni  23447  ptpjpre1  23481  ptbasfi  23491  ptpjopn  23522  dfac14  23528  txtube  23550  cnmpt11  23573  cnmpt21  23581  cnmptkp  23590  cnmptk1p  23595  qtopomap  23628  qtopcmap  23629  flimcf  23892  fclscf  23935  flfcntr  23953  ptcmplem3  23964  tgpt0  24029  tsmsi  24044  tsmsxplem2  24064  tsmsxp  24065  isucn2  24188  ucnima  24190  ucncn  24194  cfiluweak  24204  cuspcvg  24210  imasdsf1olem  24283  lpbl  24413  comet  24423  cfilucfil  24469  cnheiborlem  24875  cnheibor  24876  bndth  24879  nmoleub2lem2  25038  nmoleub3  25041  ipcau2  25156  tcphcphlem1  25157  tcphcphlem2  25158  lmmcvg  25183  cmetcaulem  25210  iscmet3lem1  25213  iscmet3lem2  25214  pjthlem1  25359  pjthlem2  25360  ivthlem1  25374  ivthlem2  25375  ivthlem3  25376  ivth2  25378  ivthle  25379  ivthle2  25380  ivthicc  25381  ovoliunlem1  25425  ovolshftlem1  25432  ovolscalem1  25436  ovolicc2lem3  25442  ovolicc2lem4  25443  ovolicc2  25445  volsup  25479  dyadmbl  25523  vitalilem2  25532  vitalilem3  25533  mbfdm  25549  ismbf3d  25577  cncombf  25581  itg2seq  25665  itg2monolem2  25674  itg2monolem3  25675  itg2mono  25676  iblitg  25691  itgconst  25742  itgfsum  25750  limcvallem  25794  cnlimci  25812  cnmptlimc  25813  dvferm1lem  25910  dvferm1  25911  dvferm2lem  25912  dvferm2  25913  dvlipcn  25921  dvle  25934  lhop1lem  25940  dvfsumge  25950  dvfsumlem2  25955  dvfsumlem2OLD  25956  dvfsumlem3  25957  ftc1a  25966  ftc1lem4  25968  itgsubstlem  25977  mdeglt  25992  deg1lt  26024  ply1divex  26064  fta1glem2  26096  fta1g  26097  plyco0  26119  plyeq0lem  26137  dgrcolem2  26202  plydivlem4  26226  plydivex  26227  fta1lem  26237  vieta1lem2  26241  vieta1  26242  tayl0  26291  ulmi  26317  ulmdvlem1  26331  ulmdvlem3  26333  ulmdv  26334  mtest  26335  pserulm  26353  efif1olem4  26476  rlimcnp  26897  rlimcnp2  26898  xrlimcnp  26900  scvxcvx  26918  lgamgulmlem5  26965  lgambdd  26969  lgamcvglem  26972  wilthlem2  27001  fsumdvdscom  27117  musumsum  27124  chtub  27145  fsumvma  27146  perfectlem2  27163  dchrelbas3  27171  dchrelbasd  27172  dchrn0  27183  dchrptlem2  27198  lgsval2lem  27240  lgsdirnn0  27277  lgsdinn0  27278  2sqlem10  27361  dchrisumlem1  27422  dchrmusum2  27427  dchrvmasumlem2  27431  dchrvmasumlem3  27432  dchrvmasumiflem1  27434  dchrisum0flblem2  27442  dchrisum0flb  27443  dchrisum0lem1b  27448  dchrisum0lem2  27451  2vmadivsumlem  27473  chpdifbndlem1  27486  selberg3lem1  27490  selberg4lem1  27493  pntrsumbnd2  27500  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem5  27514  pntrlog2bndlem6  27516  pntibndlem2  27524  pntibndlem3  27525  pntlemn  27533  pntlemj  27536  pntlemi  27537  pntlemo  27540  pntleme  27541  pntlem3  27542  pntlemp  27543  ostth2lem1  27551  ostthlem1  27560  ostth2lem2  27567  ostth3  27571  nosupprefixmo  27634  noinfprefixmo  27635  noinfbnd1lem1  27657  noinfbnd1lem4  27660  noinfbnd2lem1  27664  noinfbnd2  27665  eqscut3  27760  cofsslt  27857  coinitsslt  27858  sleadd1  27927  addsass  27943  addsbdaylem  27954  negsid  27978  mulscom  28073  addsdilem3  28087  addsdilem4  28088  mulsasslem3  28099  precsexlem8  28147  precsexlem9  28148  precsexlem11  28150  n0sfincut  28277  onsfi  28278  zs12bday  28389  tglowdim1i  28474  tglowdim2ln  28624  wlkonl1iedg  29637  wlkp1lem7  29651  wlkp1lem8  29652  crctcshwlkn0lem6  29788  eupth2eucrct  30189  eupth2lem3  30208  ubthlem1  30842  ubthlem2  30843  minvecolem3  30848  occllem  31275  pjhthlem1  31363  eqelbid  32446  fnfvor  32584  ofrco  32585  wrdt2ind  32926  mgccole1  32963  mgcmnt2  32966  dfmgc2  32969  fxpgaeq  33130  fxpsubm  33133  fxpsubg  33134  fxpsubrg  33135  elrgspnlem4  33204  elrgspnsubrunlem2  33207  0nellinds  33327  linds2eq  33338  elrspunidl  33385  prmidl  33397  mxidlmax  33422  ssmxidl  33431  1arithidomlem1  33492  1arithidom  33494  1arithufdlem3  33503  1arithufdlem4  33504  ply1dg1rt  33535  lbsdiflsp0  33631  fedgmullem1  33634  fedgmullem2  33635  extdg1id  33671  fldextrspunlsplem  33678  extdgfialglem2  33698  constrsscn  33745  constrconj  33750  zrhcntr  33984  ofcfeqd2  34106  inelpisys  34159  unelldsys  34163  ldgenpisyslem1  34168  mbfmcnvima  34260  signstfvneq0  34577  fsum2dsub  34612  hgt750lemc  34652  hgt750lemd  34653  hgt749d  34654  hgt750lemf  34658  bnj1379  34834  bnj1450  35054  revwlk  35161  subfacp1lem5  35220  cvmlift2lem10  35348  weiunfrlem  36498  weiunpo  36499  weiunso  36500  weiunfr  36501  weiunse  36502  unblimceq0lem  36540  unblimceq0  36541  unbdqndv2  36545  bj-ismoored  37141  lcmineqlem4  42065  dvle2  42105  aks4d1p9  42121  primrootlekpowne0  42138  aks6d1c1p3  42143  aks6d1c1p4  42144  aks6d1c1p5  42145  aks6d1c1  42149  hashscontpow  42155  aks6d1c2lem3  42159  sticksstones1  42179  aks6d1c6lem1  42203  aks6d1c6lem2  42204  aks6d1c6lem4  42206  aks6d1c7  42217  aks5lem3a  42222  unitscyglem1  42228  unitscyglem2  42229  unitscyglem3  42230  unitscyglem4  42231  exfinfldd  42236  fnwe2lem2  43084  aomclem4  43090  scottelrankd  44280  mnuop123d  44295  mnuprdlem1  44305  mnuprdlem2  44306  eliind  45108  rnmptbd2lem  45285  rnmptbdlem  45292  cvgcau  45528  limclner  45689  climisp  45784  climrescn  45786  climxrrelem  45787  climxrre  45788  liminflelimsuplem  45813  cncfshift  45912  cncfperiod  45917  fperdvper  45957  salunicl  46354  saldifcl  46357  meadjuni  46495  lubsscl  48991  glbsscl  48992  ipolub  49019  ipoglb  49022  ssccatid  49104  upciclem1  49198  oppcup3lem  49238  oppcthinendcALT  49473  setcthin  49497