Theorem rspcdva 3636

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068

This theorem is referenced by:  nvocnv  7317  knatar  7393  caofref  7744  caofinvl  7745  tfisi  7896  frxp2  8185  frxp3  8192  suppssov1  8238  suppssov2  8239  fpr3g  8326  fprresex  8351  wfrlem17OLD  8381  tfrlem1  8432  tfrlem5  8436  coflton  8727  cofon1  8728  cofon2  8729  marypha1lem  9502  marypha1  9503  ordtypelem6  9592  ordtypelem7  9593  wemaplem2  9616  oemapvali  9753  cantnflem1c  9756  ttrcltr  9785  ttrclss  9789  dmttrcl  9790  rnttrcl  9791  ttrclselem2  9795  infxpenlem  10082  acni  10114  dfac9  10206  dfac12lem2  10214  sornom  10346  fin1ai  10362  fin2i  10364  fin23lem11  10386  isfin2-2  10388  fin23lem17  10407  fin23lem39  10419  fin1a2lem13  10481  hsmexlem4  10498  ttukeylem5  10582  ttukeylem6  10583  canth4  10716  pwfseqlem5  10732  winalim2  10765  wununi  10775  wunpw  10776  dedekind  11453  zsupss  13002  uzwo3  13008  seqcl2  14071  seqcl  14073  seqf  14074  seqfveq2  14075  seqfveq  14077  seqshft2  14079  monoord  14083  monoord2  14084  sermono  14085  seqsplit  14086  seqcaopr3  14088  seqid  14098  seqid2  14099  seqhomo  14100  seqz  14101  discr1  14288  discr  14289  hashbclem  14501  wrdind  14770  limsupgre  15527  climi  15556  rlimi  15559  rlimclim1  15591  rlimclim  15592  climrlim2  15593  rlimcn1  15634  climcn1  15638  isercoll2  15717  caucvgrlem  15721  caucvgb  15728  iseraltlem2  15731  iseraltlem3  15732  fsumm1  15799  fsum1p  15801  fsumcom2  15822  fsumge1  15845  telfsumo  15850  telfsumo2  15851  fsumparts  15854  o1fsum  15861  isum1p  15889  isumnn0nn  15890  isumrpcl  15891  climcndslem1  15897  climcndslem2  15898  climcnds  15899  cvgrat  15931  mertenslem1  15932  mertens  15934  fprodm1  16015  fprod1p  16016  fprodcom2  16032  prmind2  16732  pcmpt2  16940  prmpwdvds  16951  prmreclem4  16966  prmreclem5  16967  vdwlem1  17028  vdwlem2  17029  vdwlem9  17036  vdwlem10  17037  rami  17062  ramcl  17076  prmodvdslcmf  17094  prmgaplcmlem1  17098  cshwsidrepsw  17141  prdsbasprj  17532  isacs2  17711  acsfiel  17712  catidex  17732  iscatd2  17739  catlid  17741  catrid  17742  subcidcl  17908  funcid  17934  yonedalem4c  18347  yonffthlem  18352  isdrs2  18376  luble  18429  glble  18442  joinle  18456  meetle  18470  poslubmo  18481  posglbmo  18482  acsdrsel  18613  isacs4lem  18614  isacs5lem  18615  acsdrscl  18616  acsficl  18617  lidrideqd  18707  grpinvalem  18711  grpinva  18712  mndind  18863  grpidd2  19017  mulgsubcl  19128  issubg4  19185  ghmf1  19286  fislw  19667  efgsdmi  19774  efgsrel  19776  gexexlem  19894  gsumzaddlem  19963  gsummhm2  19981  dprdcntz  20052  dprddisj  20053  dprdss  20073  dprd2dlem2  20084  dprd2da  20086  dpjrid  20106  ablfac1eu  20117  pgpfac1lem1  20118  pgpfaclem2  20126  lringuplu  20570  issrngd  20878  islbs2  21179  lbsextlem4  21186  prmirredlem  21506  psgndiflemB  21641  frlmphl  21824  mplsubglem  22042  mpllsslem  22043  subrgasclcl  22114  mplind  22117  evlslem1  22129  ply1scleq  22330  mdetralt  22635  mdetunilem1  22639  lmcvg  23291  iscncl  23298  lmff  23330  cnrmi  23389  cmpcov  23418  fiuncmp  23433  hauscmplem  23435  1stcfb  23474  1stcelcls  23490  restnlly  23511  islly2  23513  lly1stc  23525  kgeni  23566  ptpjpre1  23600  ptbasfi  23610  ptpjopn  23641  dfac14  23647  txtube  23669  cnmpt11  23692  cnmpt21  23700  cnmptkp  23709  cnmptk1p  23714  qtopomap  23747  qtopcmap  23748  flimcf  24011  fclscf  24054  flfcntr  24072  ptcmplem3  24083  tgpt0  24148  tsmsi  24163  tsmsxplem2  24183  tsmsxp  24184  isucn2  24309  ucnima  24311  ucncn  24315  cfiluweak  24325  cuspcvg  24331  imasdsf1olem  24404  lpbl  24537  comet  24547  cfilucfil  24593  cnheiborlem  25005  cnheibor  25006  bndth  25009  nmoleub2lem2  25168  nmoleub3  25171  ipcau2  25287  tcphcphlem1  25288  tcphcphlem2  25289  lmmcvg  25314  cmetcaulem  25341  iscmet3lem1  25344  iscmet3lem2  25345  pjthlem1  25490  pjthlem2  25491  ivthlem1  25505  ivthlem2  25506  ivthlem3  25507  ivth2  25509  ivthle  25510  ivthle2  25511  ivthicc  25512  ovoliunlem1  25556  ovolshftlem1  25563  ovolscalem1  25567  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2  25576  volsup  25610  dyadmbl  25654  vitalilem2  25663  vitalilem3  25664  mbfdm  25680  ismbf3d  25708  cncombf  25712  itg2seq  25797  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  iblitg  25823  itgconst  25874  itgfsum  25882  limcvallem  25926  cnlimci  25944  cnmptlimc  25945  dvferm1lem  26042  dvferm1  26043  dvferm2lem  26044  dvferm2  26045  dvlipcn  26053  dvle  26066  lhop1lem  26072  dvfsumge  26082  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  ftc1a  26098  ftc1lem4  26100  itgsubstlem  26109  mdeglt  26124  deg1lt  26156  ply1divex  26196  fta1glem2  26228  fta1g  26229  plyco0  26251  plyeq0lem  26269  dgrcolem2  26334  plydivlem4  26356  plydivex  26357  fta1lem  26367  vieta1lem2  26371  vieta1  26372  tayl0  26421  ulmi  26447  ulmdvlem1  26461  ulmdvlem3  26463  ulmdv  26464  mtest  26465  pserulm  26483  efif1olem4  26605  rlimcnp  27026  rlimcnp2  27027  xrlimcnp  27029  scvxcvx  27047  lgamgulmlem5  27094  lgambdd  27098  lgamcvglem  27101  wilthlem2  27130  fsumdvdscom  27246  musumsum  27253  chtub  27274  fsumvma  27275  perfectlem2  27292  dchrelbas3  27300  dchrelbasd  27301  dchrn0  27312  dchrptlem2  27327  lgsval2lem  27369  lgsdirnn0  27406  lgsdinn0  27407  2sqlem10  27490  dchrisumlem1  27551  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrisum0flblem2  27571  dchrisum0flb  27572  dchrisum0lem1b  27577  dchrisum0lem2  27580  2vmadivsumlem  27602  chpdifbndlem1  27615  selberg3lem1  27619  selberg4lem1  27622  pntrsumbnd2  27629  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntibndlem2  27653  pntibndlem3  27654  pntlemn  27662  pntlemj  27665  pntlemi  27666  pntlemo  27669  pntleme  27670  pntlem3  27671  pntlemp  27672  ostth2lem1  27680  ostthlem1  27689  ostth2lem2  27696  ostth3  27700  nosupprefixmo  27763  noinfprefixmo  27764  noinfbnd1lem1  27786  noinfbnd1lem4  27789  noinfbnd2lem1  27793  noinfbnd2  27794  cofsslt  27970  coinitsslt  27971  sleadd1  28040  addsass  28056  addsbdaylem  28067  negsid  28091  mulscom  28183  addsdilem3  28197  addsdilem4  28198  mulsasslem3  28209  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  zs12bday  28442  tglowdim1i  28527  tglowdim2ln  28677  wlkonl1iedg  29701  wlkp1lem7  29715  wlkp1lem8  29716  crctcshwlkn0lem6  29848  eupth2eucrct  30249  eupth2lem3  30268  ubthlem1  30902  ubthlem2  30903  minvecolem3  30908  occllem  31335  pjhthlem1  31423  eqelbid  32503  wrdt2ind  32920  mgccole1  32963  mgcmnt2  32966  dfmgc2  32969  chnltm1  32981  chnub  32984  0nellinds  33363  linds2eq  33374  elrspunidl  33421  prmidl  33433  mxidlmax  33458  ssmxidl  33467  1arithidomlem1  33528  1arithidom  33530  1arithufdlem3  33539  1arithufdlem4  33540  ply1dg1rt  33569  lbsdiflsp0  33639  fedgmullem1  33642  fedgmullem2  33643  extdg1id  33676  constrsscn  33730  constrconj  33735  ofcfeqd2  34065  inelpisys  34118  unelldsys  34122  ldgenpisyslem1  34127  mbfmcnvima  34220  signstfvneq0  34549  fsum2dsub  34584  hgt750lemc  34624  hgt750lemd  34625  hgt749d  34626  hgt750lemf  34630  bnj1379  34806  bnj1450  35026  revwlk  35092  subfacp1lem5  35152  cvmlift2lem10  35280  weiunfrlem  36430  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  unblimceq0lem  36472  unblimceq0  36473  unbdqndv2  36477  bj-ismoored  37073  lcmineqlem4  41989  dvle2  42029  aks4d1p9  42045  primrootlekpowne0  42062  aks6d1c1p3  42067  aks6d1c1p4  42068  aks6d1c1p5  42069  aks6d1c1  42073  hashscontpow  42079  aks6d1c2lem3  42083  sticksstones1  42103  aks6d1c6lem1  42127  aks6d1c6lem2  42128  aks6d1c6lem4  42130  aks6d1c7  42141  aks5lem3a  42146  unitscyglem1  42152  unitscyglem2  42153  unitscyglem3  42154  unitscyglem4  42155  exfinfldd  42160  fnwe2lem2  43008  aomclem4  43014  scottelrankd  44216  mnuop123d  44231  mnuprdlem1  44241  mnuprdlem2  44242  eliind  44973  rnmptbd2lem  45157  rnmptbdlem  45164  cvgcau  45406  limclner  45572  climisp  45667  climrescn  45669  climxrrelem  45670  climxrre  45671  cncfshift  45795  cncfperiod  45800  fperdvper  45840  salunicl  46237  saldifcl  46240  meadjuni  46378  lubsscl  48640  glbsscl  48641  ipolub  48660  ipoglb  48663  setcthin  48722