Theorem rspcdva 3578

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078

This theorem is used by:  nvocnv  7287  knatar  7365  caofref  7722  caofinvl  7723  tfisi  7868  frxp2  8154  frxp3  8161  suppssov1  8207  suppssov2  8208  fpr3g  8296  fprresex  8321  tfrlem1  8376  tfrlem5  8380  coflton  8673  cofon1  8674  cofon2  8675  marypha1lem  9418  marypha1  9419  ordtypelem6  9510  ordtypelem7  9511  wemaplem2  9534  oemapvali  9678  cantnflem1c  9681  ttrcltr  9710  ttrclss  9714  dmttrcl  9715  rnttrcl  9716  ttrclselem2  9720  scottelrankd  9941  infxpenlem  10085  acni  10117  dfac9  10208  dfac12lem2  10216  sornom  10348  fin1ai  10364  fin2i  10366  fin23lem11  10388  isfin2-2  10390  fin23lem17  10409  fin23lem39  10421  fin1a2lem13  10483  hsmexlem4  10500  ttukeylem5  10584  ttukeylem6  10585  canth4  10725  pwfseqlem5  10741  winalim2  10774  wununi  10784  wunpw  10785  dedekind  11466  zsupss  13057  uzwo3  13063  seqcl2  14156  seqcl  14158  seqf  14159  seqfveq2  14160  seqfveq  14162  seqshft2  14164  monoord  14168  monoord2  14169  sermono  14170  seqsplit  14171  seqcaopr3  14173  seqid  14183  seqid2  14184  seqhomo  14185  seqz  14186  discr1  14376  discr  14377  hashbclem  14590  wrdind  14864  limsupgre  15641  climi  15670  rlimi  15673  rlimclim1  15705  rlimclim  15706  climrlim2  15707  rlimcn1  15748  climcn1  15752  isercoll2  15829  caucvgrlem  15833  caucvgb  15840  iseraltlem2  15843  iseraltlem3  15844  fsumm1  15910  fsum1p  15912  fsumcom2  15933  fsumge1  15957  telfsumo  15962  telfsumo2  15963  fsumparts  15966  o1fsum  15973  isum1p  16003  isumnn0nn  16004  isumrpcl  16005  climcndslem1  16011  climcndslem2  16012  climcnds  16013  cvgrat  16045  mertenslem1  16046  mertens  16048  fprodm1  16127  fprod1p  16128  fprodcom2  16144  prmind2  16853  pcmpt2  17064  prmpwdvds  17075  prmreclem4  17090  prmreclem5  17091  vdwlem1  17152  vdwlem2  17153  vdwlem9  17160  vdwlem10  17161  rami  17186  ramcl  17200  prmodvdslcmf  17218  prmgaplcmlem1  17222  cshwsidrepsw  17264  prdsbasprj  17636  isacs2  17820  acsfiel  17821  catidex  17841  iscatd2  17848  catlid  17850  catrid  17851  subcidcl  18012  funcid  18038  yonedalem4c  18444  yonffthlem  18449  isdrs2  18473  luble  18524  glble  18537  joinle  18551  meetle  18565  poslubmo  18576  posglbmo  18577  acsdrsel  18710  isacs4lem  18711  isacs5lem  18712  acsdrscl  18713  acsficl  18714  chnltm1  18776  chnub  18789  lidrideqd  18843  grpinvalem  18847  grpinva  18848  mndind  19017  grpidd2  19181  mulgsubcl  19291  issubg4  19349  ghmf1  19453  fislw  19832  efgsdmi  19939  efgsrel  19941  gexexlem  20059  gsumzaddlem  20128  gsummhm2  20146  dprdcntz  20217  dprddisj  20218  dprdss  20238  dprd2dlem2  20249  dprd2da  20251  dpjrid  20271  ablfac1eu  20282  pgpfac1lem1  20283  pgpfaclem2  20291  lringuplu  20789  issrngd  21105  islbs2  21425  lbsextlem4  21432  prmidl  21614  prmirredlem  21771  psgndiflemB  21899  frlmphl  22080  mplsubglem  22299  mpllsslem  22300  subrgasclcl  22369  mplind  22372  evlslem1  22384  ply1scleq  22616  mdetralt  22916  mdetunilem1  22920  lmcvg  23573  iscncl  23580  lmff  23612  cnrmi  23671  cmpcov  23700  fiuncmp  23715  hauscmplem  23717  1stcfb  23756  1stcelcls  23773  restnlly  23794  islly2  23796  lly1stc  23808  kgeni  23849  ptpjpre1  23883  ptbasfi  23893  ptpjopn  23924  dfac14  23930  txtube  23952  cnmpt11  23975  cnmpt21  23983  cnmptkp  23992  cnmptk1p  23997  qtopomap  24030  qtopcmap  24031  flimcf  24294  fclscf  24337  flfcntr  24355  ptcmplem3  24366  tgpt0  24431  tsmsi  24446  tsmsxplem2  24466  tsmsxp  24467  isucn2  24590  ucnima  24592  ucncn  24596  cfiluweak  24606  cuspcvg  24612  imasdsf1olem  24685  lpbl  24815  comet  24825  cfilucfil  24871  cnheiborlem  25268  cnheibor  25269  bndth  25272  nmoleub2lem2  25430  nmoleub3  25433  ipcau2  25548  tcphcphlem1  25549  tcphcphlem2  25550  lmmcvg  25575  cmetcaulem  25602  iscmet3lem1  25605  iscmet3lem2  25606  pjthlem1  25751  pjthlem2  25752  ivthlem1  25765  ivthlem2  25766  ivthlem3  25767  ivth2  25769  ivthle  25770  ivthle2  25771  ivthicc  25772  ovoliunlem1  25816  ovolshftlem1  25823  ovolscalem1  25827  ovolicc2lem3  25833  ovolicc2lem4  25834  ovolicc2  25836  volsup  25870  dyadmbl  25914  vitalilem2  25923  vitalilem3  25924  mbfdm  25940  ismbf3d  25968  cncombf  25972  itg2seq  26056  itg2monolem2  26065  itg2monolem3  26066  itg2mono  26067  iblitg  26082  itgconst  26132  itgfsum  26140  limcvallem  26184  cnlimci  26202  cnmptlimc  26203  dvferm1lem  26297  dvferm1  26298  dvferm2lem  26299  dvferm2  26300  dvlipcn  26307  dvle  26320  lhop1lem  26326  dvfsumge  26335  dvfsumlem2  26340  dvfsumlem3  26341  ftc1a  26350  ftc1lem4  26352  itgsubstlem  26361  mdeglt  26376  deg1lt  26408  ply1divex  26448  fta1glem2  26480  fta1g  26481  plyco0  26503  plyeq0lem  26522  dgrcolem2  26586  plydivlem4  26610  plydivex  26611  fta1lem  26621  vieta1lem2  26627  vieta1  26628  tayl0  26682  ulmi  26706  ulmdvlem1  26720  ulmdvlem3  26722  ulmdv  26723  mtest  26724  pserulm  26742  efif1olem4  26866  rlimcnp  27286  rlimcnp2  27287  xrlimcnp  27289  scvxcvx  27306  lgamgulmlem5  27353  lgambdd  27357  lgamcvglem  27360  wilthlem2  27389  fsumdvdscom  27505  musumsum  27512  chtub  27532  fsumvma  27533  perfectlem2  27550  dchrelbas3  27558  dchrelbasd  27559  dchrn0  27570  dchrptlem2  27585  lgsval2lem  27627  lgsdirnn0  27664  lgsdinn0  27665  2sqlem10  27748  dchrisumlem1  27809  dchrmusum2  27814  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumiflem1  27821  dchrisum0flblem2  27829  dchrisum0flb  27830  dchrisum0lem1b  27835  dchrisum0lem2  27838  2vmadivsumlem  27860  chpdifbndlem1  27873  selberg3lem1  27877  selberg4lem1  27880  pntrsumbnd2  27887  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntibndlem2  27911  pntibndlem3  27912  pntlemn  27920  pntlemj  27923  pntlemi  27924  pntlemo  27927  pntleme  27928  pntlem3  27929  pntlemp  27930  ostth2lem1  27938  ostthlem1  27947  ostth2lem2  27954  ostth3  27958  nosupprefixmo  28050  noinfprefixmo  28051  noinfbnd1lem1  28073  noinfbnd1lem4  28076  noinfbnd2lem1  28080  noinfbnd2  28081  eqcuts3  28183  cofslts  28297  coinitslts  28298  leadds1  28368  addsass  28384  addbdaylem  28396  negsid  28420  mulscom  28518  addsdilem3  28532  addsdilem4  28533  mulsasslem3  28544  precsexlem8  28593  precsexlem9  28594  precsexlem11  28596  addonbday  28658  n0fincut  28734  onsfi  28735  bdayfinbndlem1  28846  bdayfinbnd  28848  tglowdim1i  28957  tglowdim2ln  29113  wlkonl1iedg  30237  wlkp1lem7  30251  wlkp1lem8  30252  revwlk  30260  crctcshwlkn0lem6  30397  eupth2eucrct  30811  eupth2lem3  30830  ubthlem1  31465  ubthlem2  31466  minvecolem3  31471  occllem  31898  pjhthlem1  31986  eqelbid  33064  fnfvor  33196  ofrco  33197  wrdt2ind  33509  mgccole1  33544  mgcmnt2  33547  dfmgc2  33550  fxpgaeq  33723  fxpsubm  33726  fxpsubg  33727  fxpsubrg  33728  elrgspnlem4  33799  elrgspnsubrunlem2  33802  0nellinds  33919  linds2eq  33929  elrspunidl  33971  mxidlmax  33983  ssmxidl  33992  1arithidomlem1  34060  1arithidom  34062  1arithufdlem3  34071  1arithufdlem4  34072  ply1dg1rt  34105  vietalem  34204  lbsdiflsp0  34251  fedgmullem1  34254  fedgmullem2  34255  extdg1id  34291  fldextrspunlsplem  34298  extdgfialglem2  34318  constrsscn  34365  constrconj  34370  zrhcntr  34604  ofcfeqd2  34726  inelpisys  34780  unelldsys  34784  ldgenpisyslem1  34789  mbfmcnvima  34881  signstfvneq0  35194  fsum2dsub  35229  hgt750lemc  35269  hgt750lemd  35270  hgt749d  35271  hgt750lemf  35275  bnj1379  35453  bnj1450  35673  subfacp1lem5  35928  cvmlift2lem10  36056  nmulprop  36919  nmulcom  36923  nadddilem1  36949  nadddilem3  36951  weiunfrlem  37232  weiunpo  37233  weiunso  37234  weiunfr  37235  weiunse  37236  mh-inf3f1  37309  unblimceq0lem  37352  unblimceq0  37353  unbdqndv2  37357  bj-ismoored  38008  lcmineqlem4  43062  dvle2  43102  aks4d1p9  43118  primrootlekpowne0  43135  aks6d1c1p3  43140  aks6d1c1p4  43141  aks6d1c1p5  43142  aks6d1c1  43146  hashscontpow  43152  aks6d1c2lem3  43156  sticksstones1  43176  aks6d1c6lem1  43200  aks6d1c6lem2  43201  aks6d1c6lem4  43203  aks6d1c7  43214  aks5lem3a  43219  unitscyglem1  43225  unitscyglem2  43226  unitscyglem3  43227  unitscyglem4  43228  exfinfldd  43233  fnwe2lem2  44037  aomclem4  44043  mnuop123d  45231  mnuprdlem1  45241  mnuprdlem2  45242  eliind  46057  rnmptbd2lem  46229  rnmptbdlem  46236  cvgcau  46469  limclner  46630  climisp  46725  climrescn  46727  climxrrelem  46728  climxrre  46729  liminflelimsuplem  46754  cncfshift  46853  cncfperiod  46858  fperdvper  46898  fourierdlem48  47133  salunicl  47295  saldifcl  47298  meadjuni  47436  chnerlem1  47861  lubsscl  50037  glbsscl  50038  ipolub  50065  ipoglb  50068  ssccatid  50149  upciclem1  50243  oppcup3lem  50283  oppcthinendcALT  50518  setcthin  50542  veroquadmodzerod  50953