Theorem rspcdva 3579

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 3574	. 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  7237  knatar  7313  caofref  7663  caofinvl  7664  tfisi  7811  frxp2  8096  frxp3  8103  suppssov1  8149  suppssov2  8150  fpr3g  8237  fprresex  8262  tfrlem1  8317  tfrlem5  8321  coflton  8609  cofon1  8610  cofon2  8611  marypha1lem  9348  marypha1  9349  ordtypelem6  9440  ordtypelem7  9441  wemaplem2  9464  oemapvali  9605  cantnflem1c  9608  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  infxpenlem  9935  acni  9967  dfac9  10059  dfac12lem2  10067  sornom  10199  fin1ai  10215  fin2i  10217  fin23lem11  10239  isfin2-2  10241  fin23lem17  10260  fin23lem39  10272  fin1a2lem13  10334  hsmexlem4  10351  ttukeylem5  10435  ttukeylem6  10436  canth4  10570  pwfseqlem5  10586  winalim2  10619  wununi  10629  wunpw  10630  dedekind  11308  zsupss  12862  uzwo3  12868  seqcl2  13955  seqcl  13957  seqf  13958  seqfveq2  13959  seqfveq  13961  seqshft2  13963  monoord  13967  monoord2  13968  sermono  13969  seqsplit  13970  seqcaopr3  13972  seqid  13982  seqid2  13983  seqhomo  13984  seqz  13985  discr1  14174  discr  14175  hashbclem  14387  wrdind  14657  limsupgre  15416  climi  15445  rlimi  15448  rlimclim1  15480  rlimclim  15481  climrlim2  15482  rlimcn1  15523  climcn1  15527  isercoll2  15604  caucvgrlem  15608  caucvgb  15615  iseraltlem2  15618  iseraltlem3  15619  fsumm1  15686  fsum1p  15688  fsumcom2  15709  fsumge1  15732  telfsumo  15737  telfsumo2  15738  fsumparts  15741  o1fsum  15748  isum1p  15776  isumnn0nn  15777  isumrpcl  15778  climcndslem1  15784  climcndslem2  15785  climcnds  15786  cvgrat  15818  mertenslem1  15819  mertens  15821  fprodm1  15902  fprod1p  15903  fprodcom2  15919  prmind2  16624  pcmpt2  16833  prmpwdvds  16844  prmreclem4  16859  prmreclem5  16860  vdwlem1  16921  vdwlem2  16922  vdwlem9  16929  vdwlem10  16930  rami  16955  ramcl  16969  prmodvdslcmf  16987  prmgaplcmlem1  16991  cshwsidrepsw  17033  prdsbasprj  17404  isacs2  17588  acsfiel  17589  catidex  17609  iscatd2  17616  catlid  17618  catrid  17619  subcidcl  17780  funcid  17806  yonedalem4c  18212  yonffthlem  18217  isdrs2  18241  luble  18292  glble  18305  joinle  18319  meetle  18333  poslubmo  18344  posglbmo  18345  acsdrsel  18478  isacs4lem  18479  isacs5lem  18480  acsdrscl  18481  acsficl  18482  chnltm1  18544  chnub  18557  lidrideqd  18606  grpinvalem  18610  grpinva  18611  mndind  18765  grpidd2  18919  mulgsubcl  19030  issubg4  19087  ghmf1  19187  fislw  19566  efgsdmi  19673  efgsrel  19675  gexexlem  19793  gsumzaddlem  19862  gsummhm2  19880  dprdcntz  19951  dprddisj  19952  dprdss  19972  dprd2dlem2  19983  dprd2da  19985  dpjrid  20005  ablfac1eu  20016  pgpfac1lem1  20017  pgpfaclem2  20025  lringuplu  20489  issrngd  20800  islbs2  21121  lbsextlem4  21128  prmirredlem  21439  psgndiflemB  21567  frlmphl  21748  mplsubglem  21966  mpllsslem  21967  subrgasclcl  22034  mplind  22037  evlslem1  22049  ply1scleq  22261  mdetralt  22564  mdetunilem1  22568  lmcvg  23218  iscncl  23225  lmff  23257  cnrmi  23316  cmpcov  23345  fiuncmp  23360  hauscmplem  23362  1stcfb  23401  1stcelcls  23417  restnlly  23438  islly2  23440  lly1stc  23452  kgeni  23493  ptpjpre1  23527  ptbasfi  23537  ptpjopn  23568  dfac14  23574  txtube  23596  cnmpt11  23619  cnmpt21  23627  cnmptkp  23636  cnmptk1p  23641  qtopomap  23674  qtopcmap  23675  flimcf  23938  fclscf  23981  flfcntr  23999  ptcmplem3  24010  tgpt0  24075  tsmsi  24090  tsmsxplem2  24110  tsmsxp  24111  isucn2  24234  ucnima  24236  ucncn  24240  cfiluweak  24250  cuspcvg  24256  imasdsf1olem  24329  lpbl  24459  comet  24469  cfilucfil  24515  cnheiborlem  24921  cnheibor  24922  bndth  24925  nmoleub2lem2  25084  nmoleub3  25087  ipcau2  25202  tcphcphlem1  25203  tcphcphlem2  25204  lmmcvg  25229  cmetcaulem  25256  iscmet3lem1  25259  iscmet3lem2  25260  pjthlem1  25405  pjthlem2  25406  ivthlem1  25420  ivthlem2  25421  ivthlem3  25422  ivth2  25424  ivthle  25425  ivthle2  25426  ivthicc  25427  ovoliunlem1  25471  ovolshftlem1  25478  ovolscalem1  25482  ovolicc2lem3  25488  ovolicc2lem4  25489  ovolicc2  25491  volsup  25525  dyadmbl  25569  vitalilem2  25578  vitalilem3  25579  mbfdm  25595  ismbf3d  25623  cncombf  25627  itg2seq  25711  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  iblitg  25737  itgconst  25788  itgfsum  25796  limcvallem  25840  cnlimci  25858  cnmptlimc  25859  dvferm1lem  25956  dvferm1  25957  dvferm2lem  25958  dvferm2  25959  dvlipcn  25967  dvle  25980  lhop1lem  25986  dvfsumge  25996  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  ftc1a  26012  ftc1lem4  26014  itgsubstlem  26023  mdeglt  26038  deg1lt  26070  ply1divex  26110  fta1glem2  26142  fta1g  26143  plyco0  26165  plyeq0lem  26183  dgrcolem2  26248  plydivlem4  26272  plydivex  26273  fta1lem  26283  vieta1lem2  26287  vieta1  26288  tayl0  26337  ulmi  26363  ulmdvlem1  26377  ulmdvlem3  26379  ulmdv  26380  mtest  26381  pserulm  26399  efif1olem4  26522  rlimcnp  26943  rlimcnp2  26944  xrlimcnp  26946  scvxcvx  26964  lgamgulmlem5  27011  lgambdd  27015  lgamcvglem  27018  wilthlem2  27047  fsumdvdscom  27163  musumsum  27170  chtub  27191  fsumvma  27192  perfectlem2  27209  dchrelbas3  27217  dchrelbasd  27218  dchrn0  27229  dchrptlem2  27244  lgsval2lem  27286  lgsdirnn0  27323  lgsdinn0  27324  2sqlem10  27407  dchrisumlem1  27468  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrisum0flblem2  27488  dchrisum0flb  27489  dchrisum0lem1b  27494  dchrisum0lem2  27497  2vmadivsumlem  27519  chpdifbndlem1  27532  selberg3lem1  27536  selberg4lem1  27539  pntrsumbnd2  27546  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntibndlem2  27570  pntibndlem3  27571  pntlemn  27579  pntlemj  27582  pntlemi  27583  pntlemo  27586  pntleme  27587  pntlem3  27588  pntlemp  27589  ostth2lem1  27597  ostthlem1  27606  ostth2lem2  27613  ostth3  27617  nosupprefixmo  27680  noinfprefixmo  27681  noinfbnd1lem1  27703  noinfbnd1lem4  27706  noinfbnd2lem1  27710  noinfbnd2  27711  eqcuts3  27812  cofslts  27926  coinitslts  27927  leadds1  27997  addsass  28013  addbdaylem  28025  negsid  28049  mulscom  28147  addsdilem3  28161  addsdilem4  28162  mulsasslem3  28173  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  addonbday  28287  n0fincut  28363  onsfi  28364  bdayfinbndlem1  28475  bdayfinbnd  28477  tglowdim1i  28585  tglowdim2ln  28735  wlkonl1iedg  29749  wlkp1lem7  29763  wlkp1lem8  29764  crctcshwlkn0lem6  29900  eupth2eucrct  30304  eupth2lem3  30323  ubthlem1  30957  ubthlem2  30958  minvecolem3  30963  occllem  31390  pjhthlem1  31478  eqelbid  32560  fnfvor  32698  ofrco  32699  wrdt2ind  33045  mgccole1  33082  mgcmnt2  33085  dfmgc2  33088  fxpgaeq  33262  fxpsubm  33265  fxpsubg  33266  fxpsubrg  33267  elrgspnlem4  33338  elrgspnsubrunlem2  33341  0nellinds  33462  linds2eq  33473  elrspunidl  33520  prmidl  33532  mxidlmax  33557  ssmxidl  33566  1arithidomlem1  33627  1arithidom  33629  1arithufdlem3  33638  1arithufdlem4  33639  ply1dg1rt  33672  vietalem  33755  lbsdiflsp0  33803  fedgmullem1  33806  fedgmullem2  33807  extdg1id  33843  fldextrspunlsplem  33850  extdgfialglem2  33870  constrsscn  33917  constrconj  33922  zrhcntr  34156  ofcfeqd2  34278  inelpisys  34331  unelldsys  34335  ldgenpisyslem1  34340  mbfmcnvima  34432  signstfvneq0  34749  fsum2dsub  34784  hgt750lemc  34824  hgt750lemd  34825  hgt749d  34826  hgt750lemf  34830  bnj1379  35005  bnj1450  35225  revwlk  35338  subfacp1lem5  35397  cvmlift2lem10  35525  weiunfrlem  36677  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  unblimceq0lem  36725  unblimceq0  36726  unbdqndv2  36730  bj-ismoored  37357  lcmineqlem4  42399  dvle2  42439  aks4d1p9  42455  primrootlekpowne0  42472  aks6d1c1p3  42477  aks6d1c1p4  42478  aks6d1c1p5  42479  aks6d1c1  42483  hashscontpow  42489  aks6d1c2lem3  42493  sticksstones1  42513  aks6d1c6lem1  42537  aks6d1c6lem2  42538  aks6d1c6lem4  42540  aks6d1c7  42551  aks5lem3a  42556  unitscyglem1  42562  unitscyglem2  42563  unitscyglem3  42564  unitscyglem4  42565  exfinfldd  42570  fnwe2lem2  43405  aomclem4  43411  scottelrankd  44600  mnuop123d  44615  mnuprdlem1  44625  mnuprdlem2  44626  eliind  45428  rnmptbd2lem  45603  rnmptbdlem  45610  cvgcau  45845  limclner  46006  climisp  46101  climrescn  46103  climxrrelem  46104  climxrre  46105  liminflelimsuplem  46130  cncfshift  46229  cncfperiod  46234  fperdvper  46274  salunicl  46671  saldifcl  46674  meadjuni  46812  chnerlem1  47237  lubsscl  49316  glbsscl  49317  ipolub  49344  ipoglb  49347  ssccatid  49428  upciclem1  49522  oppcup3lem  49562  oppcthinendcALT  49797  setcthin  49821