Theorem rspcdva 3581

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081

This theorem is used by:  nvocnv  7320  knatar  7398  caofref  7756  caofinvl  7757  tfisi  7904  fnwe2lem3  8184  frxp2  8198  frxp3  8205  suppssov1  8252  suppssov2  8253  fpr3g  8341  fprresex  8366  tfrlem1  8421  tfrlem5  8425  coflton  8718  cofon1  8719  cofon2  8720  marypha1lem  9462  marypha1  9463  ordtypelem6  9554  ordtypelem7  9555  wemaplem2  9578  oemapvali  9722  cantnflem1c  9725  ttrcltr  9754  ttrclss  9758  dmttrcl  9759  rnttrcl  9760  ttrclselem2  9764  scottelrankd  9985  infxpenlem  10131  acni  10163  dfac9  10254  dfac12lem2  10262  sornom  10394  fin1ai  10410  fin2i  10412  fin23lem11  10434  isfin2-2  10436  fin23lem17  10455  fin23lem39  10467  fin1a2lem13  10529  hsmexlem4  10546  ttukeylem5  10630  ttukeylem6  10631  canth4  10771  pwfseqlem5  10787  winalim2  10820  wununi  10830  wunpw  10831  dedekind  11512  zsupss  13104  uzwo3  13110  seqcl2  14203  seqcl  14205  seqf  14206  seqfveq2  14207  seqfveq  14209  seqshft2  14211  monoord  14215  monoord2  14216  sermono  14217  seqsplit  14218  seqcaopr3  14220  seqid  14230  seqid2  14231  seqhomo  14232  seqz  14233  discr1  14424  discr  14425  hashbclem  14638  wrdind  14913  limsupgre  15692  climi  15721  rlimi  15724  rlimclim1  15756  rlimclim  15757  climrlim2  15758  rlimcn1  15799  climcn1  15803  isercoll2  15880  caucvgrlem  15884  caucvgb  15891  iseraltlem2  15894  iseraltlem3  15895  fsumm1  15961  fsum1p  15963  fsumcom2  15984  fsumge1  16008  telfsumo  16013  telfsumo2  16014  fsumparts  16017  o1fsum  16024  isum1p  16054  isumnn0nn  16055  isumrpcl  16056  climcndslem1  16062  climcndslem2  16063  climcnds  16064  cvgrat  16096  mertenslem1  16097  mertens  16099  fprodm1  16178  fprod1p  16179  fprodcom2  16195  prmind2  16904  pcmpt2  17115  prmpwdvds  17126  prmreclem4  17141  prmreclem5  17142  vdwlem1  17203  vdwlem2  17204  vdwlem9  17211  vdwlem10  17212  rami  17237  ramcl  17251  prmodvdslcmf  17269  prmgaplcmlem1  17273  cshwsidrepsw  17315  prdsbasprj  17693  isacs2  17877  acsfiel  17878  catidex  17898  iscatd2  17905  catlid  17907  catrid  17908  subcidcl  18069  funcid  18095  yonedalem4c  18501  yonffthlem  18506  isdrs2  18530  luble  18581  glble  18594  joinle  18608  meetle  18622  poslubmo  18633  posglbmo  18634  acsdrsel  18767  isacs4lem  18768  isacs5lem  18769  acsdrscl  18770  acsficl  18771  chnltm1  18833  chnub  18846  lidrideqd  18900  grpinvalem  18904  grpinva  18905  mndind  19074  grpidd2  19238  mulgsubcl  19348  issubg4  19406  ghmf1  19510  fislw  19890  efgsdmi  19997  efgsrel  19999  gexexlem  20117  gsumzaddlem  20186  gsummhm2  20204  dprdcntz  20275  dprddisj  20276  dprdss  20296  dprd2dlem2  20307  dprd2da  20309  dpjrid  20329  ablfac1eu  20340  pgpfac1lem1  20341  pgpfaclem2  20349  lringuplu  20847  issrngd  21163  islbs2  21483  lbsextlem4  21490  prmidl  21672  prmirredlem  21833  psgndiflemB  21961  frlmphl  22142  mplsubglem  22361  mpllsslem  22362  subrgasclcl  22431  mplind  22434  evlslem1  22446  ply1scleq  22678  mdetralt  22978  mdetunilem1  22982  lmcvg  23635  iscncl  23642  lmff  23674  cnrmi  23733  cmpcov  23762  fiuncmp  23777  hauscmplem  23779  1stcfb  23818  1stcelcls  23835  restnlly  23856  islly2  23858  lly1stc  23870  kgeni  23911  ptpjpre1  23945  ptbasfi  23955  ptpjopn  23986  dfac14  23992  txtube  24014  cnmpt11  24037  cnmpt21  24045  cnmptkp  24054  cnmptk1p  24059  qtopomap  24092  qtopcmap  24093  flimcf  24356  fclscf  24399  flfcntr  24417  ptcmplem3  24428  tgpt0  24493  tsmsi  24508  tsmsxplem2  24528  tsmsxp  24529  isucn2  24652  ucnima  24654  ucncn  24658  cfiluweak  24668  cuspcvg  24674  imasdsf1olem  24747  lpbl  24877  comet  24887  cfilucfil  24933  cnheiborlem  25330  cnheibor  25331  bndth  25334  nmoleub2lem2  25492  nmoleub3  25495  ipcau2  25610  tcphcphlem1  25611  tcphcphlem2  25612  lmmcvg  25637  cmetcaulem  25664  iscmet3lem1  25667  iscmet3lem2  25668  pjthlem1  25813  pjthlem2  25814  ivthlem1  25827  ivthlem2  25828  ivthlem3  25829  ivth2  25831  ivthle  25832  ivthle2  25833  ivthicc  25834  ovoliunlem1  25878  ovolshftlem1  25885  ovolscalem1  25889  ovolicc2lem3  25895  ovolicc2lem4  25896  ovolicc2  25898  volsup  25932  dyadmbl  25976  vitalilem2  25985  vitalilem3  25986  mbfdm  26002  ismbf3d  26030  cncombf  26034  itg2seq  26118  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  iblitg  26144  itgconst  26194  itgfsum  26202  limcvallem  26246  cnlimci  26264  cnmptlimc  26265  dvferm1lem  26359  dvferm1  26360  dvferm2lem  26361  dvferm2  26362  dvlipcn  26369  dvle  26382  lhop1lem  26388  dvfsumge  26397  dvfsumlem2  26402  dvfsumlem3  26403  ftc1a  26412  ftc1lem4  26414  itgsubstlem  26423  mdeglt  26438  deg1lt  26470  ply1divex  26510  fta1glem2  26542  fta1g  26543  plyco0  26565  plyeq0lem  26584  dgrcolem2  26648  plydivlem4  26672  plydivex  26673  fta1lem  26683  vieta1lem2  26689  vieta1  26690  tayl0  26746  ulmi  26770  ulmdvlem1  26784  ulmdvlem3  26786  ulmdv  26787  mtest  26788  pserulm  26806  efif1olem4  26930  rlimcnp  27350  rlimcnp2  27351  xrlimcnp  27353  scvxcvx  27370  lgamgulmlem5  27417  lgambdd  27421  lgamcvglem  27424  wilthlem2  27453  fsumdvdscom  27569  musumsum  27576  chtub  27596  fsumvma  27597  perfectlem2  27614  dchrelbas3  27622  dchrelbasd  27623  dchrn0  27634  dchrptlem2  27649  lgsval2lem  27691  lgsdirnn0  27728  lgsdinn0  27729  2sqlem10  27812  dchrisumlem1  27873  dchrmusum2  27878  dchrvmasumlem2  27882  dchrvmasumlem3  27883  dchrvmasumiflem1  27885  dchrisum0flblem2  27893  dchrisum0flb  27894  dchrisum0lem1b  27899  dchrisum0lem2  27902  2vmadivsumlem  27924  chpdifbndlem1  27937  selberg3lem1  27941  selberg4lem1  27944  pntrsumbnd2  27951  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntibndlem2  27975  pntibndlem3  27976  pntlemn  27984  pntlemj  27987  pntlemi  27988  pntlemo  27991  pntleme  27992  pntlem3  27993  pntlemp  27994  ostth2lem1  28002  ostthlem1  28011  ostth2lem2  28018  ostth3  28022  nosupprefixmo  28114  noinfprefixmo  28115  noinfbnd1lem1  28137  noinfbnd1lem4  28140  noinfbnd2lem1  28144  noinfbnd2  28145  eqcuts3  28247  cofslts  28361  coinitslts  28362  leadds1  28432  addsass  28448  addbdaylem  28460  negsid  28484  mulscom  28582  addsdilem3  28596  addsdilem4  28597  mulsasslem3  28608  precsexlem8  28657  precsexlem9  28658  precsexlem11  28660  addonbday  28722  n0fincut  28798  onsfi  28799  bdayfinbndlem1  28910  bdayfinbnd  28912  tglowdim1i  29021  tglowdim2ln  29177  wlkonl1iedg  30301  wlkp1lem7  30315  wlkp1lem8  30316  revwlk  30324  crctcshwlkn0lem6  30461  eupth2eucrct  30875  eupth2lem3  30894  ubthlem1  31529  ubthlem2  31530  minvecolem3  31535  occllem  31962  pjhthlem1  32050  eqelbid  33170  fnfvor  33301  ofrco  33302  wrdt2ind  33612  mgccole1  33650  mgcmnt2  33653  dfmgc2  33656  fxpgaeq  33829  fxpsubm  33832  fxpsubg  33833  fxpsubrg  33834  elrgspnlem4  33905  elrgspnsubrunlem2  33908  0nellinds  34030  linds2eq  34040  elrspunidl  34082  mxidlmax  34094  ssmxidl  34103  1arithidomlem1  34171  1arithidom  34173  1arithufdlem3  34182  1arithufdlem4  34183  ply1dg1rt  34215  vietalem  34322  lbsdiflsp0  34369  fedgmullem1  34372  fedgmullem2  34373  extdg1id  34409  fldextrspunlsplem  34416  extdgfialglem2  34436  constrsscn  34483  constrconj  34488  zrhcntr  34722  ofcfeqd2  34844  inelpisys  34898  unelldsys  34902  ldgenpisyslem1  34907  mbfmcnvima  34999  signstfvneq0  35312  fsum2dsub  35347  hgt750lemc  35387  hgt750lemd  35388  hgt749d  35389  hgt750lemf  35393  bnj1379  35571  bnj1450  35791  subfacp1lem5  36157  cvmlift2lem10  36285  nmulprop  37154  nmulcom  37158  nadddilem1  37184  nadddilem3  37186  weiunfrlem  37467  weiunpo  37468  weiunso  37469  weiunfr  37470  weiunse  37471  mh-inf3f1  37544  unblimceq0lem  37587  unblimceq0  37588  unbdqndv2  37592  bj-ismoored  38298  lcmineqlem4  43348  dvle2  43388  aks4d1p9  43404  primrootlekpowne0  43421  aks6d1c1p3  43426  aks6d1c1p4  43427  aks6d1c1p5  43428  aks6d1c1  43432  hashscontpow  43438  aks6d1c2lem3  43442  sticksstones1  43462  aks6d1c6lem1  43486  aks6d1c6lem2  43487  aks6d1c6lem4  43489  aks6d1c7  43500  aks5lem3a  43505  unitscyglem1  43511  unitscyglem2  43512  unitscyglem3  43513  unitscyglem4  43514  exfinfldd  43519  aomclem4  44325  mnuop123d  45507  mnuprdlem1  45517  mnuprdlem2  45518  eliind  46362  rnmptbd2lem  46533  rnmptbdlem  46540  cvgcau  46773  limclner  46934  climisp  47029  climrescn  47031  climxrrelem  47032  climxrre  47033  liminflelimsuplem  47058  cncfshift  47157  cncfperiod  47162  fperdvper  47202  fourierdlem48  47437  salunicl  47599  saldifcl  47602  meadjuni  47740  chnerlem1  48165  lubsscl  50405  glbsscl  50406  ipolub  50433  ipoglb  50436  ssccatid  50517  upciclem1  50613  oppcup3lem  50653  oppcthinendcALT  50907  setcthin  50931  veroquadmodzerod  51412