Theorem rspcdva 3589

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 3584	. 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  7256  knatar  7332  caofref  7684  caofinvl  7685  tfisi  7835  frxp2  8123  frxp3  8130  suppssov1  8176  suppssov2  8177  fpr3g  8264  fprresex  8289  tfrlem1  8344  tfrlem5  8348  coflton  8635  cofon1  8636  cofon2  8637  marypha1lem  9384  marypha1  9385  ordtypelem6  9476  ordtypelem7  9477  wemaplem2  9500  oemapvali  9637  cantnflem1c  9640  ttrcltr  9669  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  infxpenlem  9966  acni  9998  dfac9  10090  dfac12lem2  10098  sornom  10230  fin1ai  10246  fin2i  10248  fin23lem11  10270  isfin2-2  10272  fin23lem17  10291  fin23lem39  10303  fin1a2lem13  10365  hsmexlem4  10382  ttukeylem5  10466  ttukeylem6  10467  canth4  10600  pwfseqlem5  10616  winalim2  10649  wununi  10659  wunpw  10660  dedekind  11337  zsupss  12896  uzwo3  12902  seqcl2  13985  seqcl  13987  seqf  13988  seqfveq2  13989  seqfveq  13991  seqshft2  13993  monoord  13997  monoord2  13998  sermono  13999  seqsplit  14000  seqcaopr3  14002  seqid  14012  seqid2  14013  seqhomo  14014  seqz  14015  discr1  14204  discr  14205  hashbclem  14417  wrdind  14687  limsupgre  15447  climi  15476  rlimi  15479  rlimclim1  15511  rlimclim  15512  climrlim2  15513  rlimcn1  15554  climcn1  15558  isercoll2  15635  caucvgrlem  15639  caucvgb  15646  iseraltlem2  15649  iseraltlem3  15650  fsumm1  15717  fsum1p  15719  fsumcom2  15740  fsumge1  15763  telfsumo  15768  telfsumo2  15769  fsumparts  15772  o1fsum  15779  isum1p  15807  isumnn0nn  15808  isumrpcl  15809  climcndslem1  15815  climcndslem2  15816  climcnds  15817  cvgrat  15849  mertenslem1  15850  mertens  15852  fprodm1  15933  fprod1p  15934  fprodcom2  15950  prmind2  16655  pcmpt2  16864  prmpwdvds  16875  prmreclem4  16890  prmreclem5  16891  vdwlem1  16952  vdwlem2  16953  vdwlem9  16960  vdwlem10  16961  rami  16986  ramcl  17000  prmodvdslcmf  17018  prmgaplcmlem1  17022  cshwsidrepsw  17064  prdsbasprj  17435  isacs2  17614  acsfiel  17615  catidex  17635  iscatd2  17642  catlid  17644  catrid  17645  subcidcl  17806  funcid  17832  yonedalem4c  18238  yonffthlem  18243  isdrs2  18267  luble  18318  glble  18331  joinle  18345  meetle  18359  poslubmo  18370  posglbmo  18371  acsdrsel  18502  isacs4lem  18503  isacs5lem  18504  acsdrscl  18505  acsficl  18506  lidrideqd  18596  grpinvalem  18600  grpinva  18601  mndind  18755  grpidd2  18909  mulgsubcl  19020  issubg4  19077  ghmf1  19178  fislw  19555  efgsdmi  19662  efgsrel  19664  gexexlem  19782  gsumzaddlem  19851  gsummhm2  19869  dprdcntz  19940  dprddisj  19941  dprdss  19961  dprd2dlem2  19972  dprd2da  19974  dpjrid  19994  ablfac1eu  20005  pgpfac1lem1  20006  pgpfaclem2  20014  lringuplu  20453  issrngd  20764  islbs2  21064  lbsextlem4  21071  prmirredlem  21382  psgndiflemB  21509  frlmphl  21690  mplsubglem  21908  mpllsslem  21909  subrgasclcl  21974  mplind  21977  evlslem1  21989  ply1scleq  22192  mdetralt  22495  mdetunilem1  22499  lmcvg  23149  iscncl  23156  lmff  23188  cnrmi  23247  cmpcov  23276  fiuncmp  23291  hauscmplem  23293  1stcfb  23332  1stcelcls  23348  restnlly  23369  islly2  23371  lly1stc  23383  kgeni  23424  ptpjpre1  23458  ptbasfi  23468  ptpjopn  23499  dfac14  23505  txtube  23527  cnmpt11  23550  cnmpt21  23558  cnmptkp  23567  cnmptk1p  23572  qtopomap  23605  qtopcmap  23606  flimcf  23869  fclscf  23912  flfcntr  23930  ptcmplem3  23941  tgpt0  24006  tsmsi  24021  tsmsxplem2  24041  tsmsxp  24042  isucn2  24166  ucnima  24168  ucncn  24172  cfiluweak  24182  cuspcvg  24188  imasdsf1olem  24261  lpbl  24391  comet  24401  cfilucfil  24447  cnheiborlem  24853  cnheibor  24854  bndth  24857  nmoleub2lem2  25016  nmoleub3  25019  ipcau2  25134  tcphcphlem1  25135  tcphcphlem2  25136  lmmcvg  25161  cmetcaulem  25188  iscmet3lem1  25191  iscmet3lem2  25192  pjthlem1  25337  pjthlem2  25338  ivthlem1  25352  ivthlem2  25353  ivthlem3  25354  ivth2  25356  ivthle  25357  ivthle2  25358  ivthicc  25359  ovoliunlem1  25403  ovolshftlem1  25410  ovolscalem1  25414  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2  25423  volsup  25457  dyadmbl  25501  vitalilem2  25510  vitalilem3  25511  mbfdm  25527  ismbf3d  25555  cncombf  25559  itg2seq  25643  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  iblitg  25669  itgconst  25720  itgfsum  25728  limcvallem  25772  cnlimci  25790  cnmptlimc  25791  dvferm1lem  25888  dvferm1  25889  dvferm2lem  25890  dvferm2  25891  dvlipcn  25899  dvle  25912  lhop1lem  25918  dvfsumge  25928  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  ftc1a  25944  ftc1lem4  25946  itgsubstlem  25955  mdeglt  25970  deg1lt  26002  ply1divex  26042  fta1glem2  26074  fta1g  26075  plyco0  26097  plyeq0lem  26115  dgrcolem2  26180  plydivlem4  26204  plydivex  26205  fta1lem  26215  vieta1lem2  26219  vieta1  26220  tayl0  26269  ulmi  26295  ulmdvlem1  26309  ulmdvlem3  26311  ulmdv  26312  mtest  26313  pserulm  26331  efif1olem4  26454  rlimcnp  26875  rlimcnp2  26876  xrlimcnp  26878  scvxcvx  26896  lgamgulmlem5  26943  lgambdd  26947  lgamcvglem  26950  wilthlem2  26979  fsumdvdscom  27095  musumsum  27102  chtub  27123  fsumvma  27124  perfectlem2  27141  dchrelbas3  27149  dchrelbasd  27150  dchrn0  27161  dchrptlem2  27176  lgsval2lem  27218  lgsdirnn0  27255  lgsdinn0  27256  2sqlem10  27339  dchrisumlem1  27400  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  dchrisum0flb  27421  dchrisum0lem1b  27426  dchrisum0lem2  27429  2vmadivsumlem  27451  chpdifbndlem1  27464  selberg3lem1  27468  selberg4lem1  27471  pntrsumbnd2  27478  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntibndlem2  27502  pntibndlem3  27503  pntlemn  27511  pntlemj  27514  pntlemi  27515  pntlemo  27518  pntleme  27519  pntlem3  27520  pntlemp  27521  ostth2lem1  27529  ostthlem1  27538  ostth2lem2  27545  ostth3  27549  nosupprefixmo  27612  noinfprefixmo  27613  noinfbnd1lem1  27635  noinfbnd1lem4  27638  noinfbnd2lem1  27642  noinfbnd2  27643  cofsslt  27826  coinitsslt  27827  sleadd1  27896  addsass  27912  addsbdaylem  27923  negsid  27947  mulscom  28042  addsdilem3  28056  addsdilem4  28057  mulsasslem3  28068  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  n0sfincut  28246  onsfi  28247  zs12bday  28343  tglowdim1i  28428  tglowdim2ln  28578  wlkonl1iedg  29593  wlkp1lem7  29607  wlkp1lem8  29608  crctcshwlkn0lem6  29745  eupth2eucrct  30146  eupth2lem3  30165  ubthlem1  30799  ubthlem2  30800  minvecolem3  30805  occllem  31232  pjhthlem1  31320  eqelbid  32404  wrdt2ind  32875  mgccole1  32916  mgcmnt2  32919  dfmgc2  32922  chnltm1  32934  chnub  32938  fxpgaeq  33126  fxpsubm  33129  elrgspnlem4  33196  elrgspnsubrunlem2  33199  0nellinds  33341  linds2eq  33352  elrspunidl  33399  prmidl  33411  mxidlmax  33436  ssmxidl  33445  1arithidomlem1  33506  1arithidom  33508  1arithufdlem3  33517  1arithufdlem4  33518  ply1dg1rt  33548  lbsdiflsp0  33622  fedgmullem1  33625  fedgmullem2  33626  extdg1id  33661  fldextrspunlsplem  33668  constrsscn  33730  constrconj  33735  zrhcntr  33969  ofcfeqd2  34091  inelpisys  34144  unelldsys  34148  ldgenpisyslem1  34153  mbfmcnvima  34246  signstfvneq0  34563  fsum2dsub  34598  hgt750lemc  34638  hgt750lemd  34639  hgt749d  34640  hgt750lemf  34644  bnj1379  34820  bnj1450  35040  revwlk  35112  subfacp1lem5  35171  cvmlift2lem10  35299  weiunfrlem  36452  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  unblimceq0lem  36494  unblimceq0  36495  unbdqndv2  36499  bj-ismoored  37095  lcmineqlem4  42020  dvle2  42060  aks4d1p9  42076  primrootlekpowne0  42093  aks6d1c1p3  42098  aks6d1c1p4  42099  aks6d1c1p5  42100  aks6d1c1  42104  hashscontpow  42110  aks6d1c2lem3  42114  sticksstones1  42134  aks6d1c6lem1  42158  aks6d1c6lem2  42159  aks6d1c6lem4  42161  aks6d1c7  42172  aks5lem3a  42177  unitscyglem1  42183  unitscyglem2  42184  unitscyglem3  42185  unitscyglem4  42186  exfinfldd  42191  fnwe2lem2  43040  aomclem4  43046  scottelrankd  44236  mnuop123d  44251  mnuprdlem1  44261  mnuprdlem2  44262  eliind  45065  rnmptbd2lem  45242  rnmptbdlem  45249  cvgcau  45486  limclner  45649  climisp  45744  climrescn  45746  climxrrelem  45747  climxrre  45748  liminflelimsuplem  45773  cncfshift  45872  cncfperiod  45877  fperdvper  45917  salunicl  46314  saldifcl  46317  meadjuni  46455  lubsscl  48948  glbsscl  48949  ipolub  48976  ipoglb  48979  ssccatid  49061  upciclem1  49155  oppcup3lem  49195  oppcthinendcALT  49430  setcthin  49454