Theorem rspcdva 3577

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  nvocnv  7227  knatar  7303  caofref  7653  caofinvl  7654  tfisi  7801  frxp2  8086  frxp3  8093  suppssov1  8139  suppssov2  8140  fpr3g  8227  fprresex  8252  tfrlem1  8307  tfrlem5  8311  coflton  8599  cofon1  8600  cofon2  8601  marypha1lem  9336  marypha1  9337  ordtypelem6  9428  ordtypelem7  9429  wemaplem2  9452  oemapvali  9593  cantnflem1c  9596  ttrcltr  9625  ttrclss  9629  dmttrcl  9630  rnttrcl  9631  ttrclselem2  9635  infxpenlem  9923  acni  9955  dfac9  10047  dfac12lem2  10055  sornom  10187  fin1ai  10203  fin2i  10205  fin23lem11  10227  isfin2-2  10229  fin23lem17  10248  fin23lem39  10260  fin1a2lem13  10322  hsmexlem4  10339  ttukeylem5  10423  ttukeylem6  10424  canth4  10558  pwfseqlem5  10574  winalim2  10607  wununi  10617  wunpw  10618  dedekind  11296  zsupss  12850  uzwo3  12856  seqcl2  13943  seqcl  13945  seqf  13946  seqfveq2  13947  seqfveq  13949  seqshft2  13951  monoord  13955  monoord2  13956  sermono  13957  seqsplit  13958  seqcaopr3  13960  seqid  13970  seqid2  13971  seqhomo  13972  seqz  13973  discr1  14162  discr  14163  hashbclem  14375  wrdind  14645  limsupgre  15404  climi  15433  rlimi  15436  rlimclim1  15468  rlimclim  15469  climrlim2  15470  rlimcn1  15511  climcn1  15515  isercoll2  15592  caucvgrlem  15596  caucvgb  15603  iseraltlem2  15606  iseraltlem3  15607  fsumm1  15674  fsum1p  15676  fsumcom2  15697  fsumge1  15720  telfsumo  15725  telfsumo2  15726  fsumparts  15729  o1fsum  15736  isum1p  15764  isumnn0nn  15765  isumrpcl  15766  climcndslem1  15772  climcndslem2  15773  climcnds  15774  cvgrat  15806  mertenslem1  15807  mertens  15809  fprodm1  15890  fprod1p  15891  fprodcom2  15907  prmind2  16612  pcmpt2  16821  prmpwdvds  16832  prmreclem4  16847  prmreclem5  16848  vdwlem1  16909  vdwlem2  16910  vdwlem9  16917  vdwlem10  16918  rami  16943  ramcl  16957  prmodvdslcmf  16975  prmgaplcmlem1  16979  cshwsidrepsw  17021  prdsbasprj  17392  isacs2  17576  acsfiel  17577  catidex  17597  iscatd2  17604  catlid  17606  catrid  17607  subcidcl  17768  funcid  17794  yonedalem4c  18200  yonffthlem  18205  isdrs2  18229  luble  18280  glble  18293  joinle  18307  meetle  18321  poslubmo  18332  posglbmo  18333  acsdrsel  18466  isacs4lem  18467  isacs5lem  18468  acsdrscl  18469  acsficl  18470  chnltm1  18532  chnub  18545  lidrideqd  18594  grpinvalem  18598  grpinva  18599  mndind  18753  grpidd2  18907  mulgsubcl  19018  issubg4  19075  ghmf1  19175  fislw  19554  efgsdmi  19661  efgsrel  19663  gexexlem  19781  gsumzaddlem  19850  gsummhm2  19868  dprdcntz  19939  dprddisj  19940  dprdss  19960  dprd2dlem2  19971  dprd2da  19973  dpjrid  19993  ablfac1eu  20004  pgpfac1lem1  20005  pgpfaclem2  20013  lringuplu  20477  issrngd  20788  islbs2  21109  lbsextlem4  21116  prmirredlem  21427  psgndiflemB  21555  frlmphl  21736  mplsubglem  21954  mpllsslem  21955  subrgasclcl  22022  mplind  22025  evlslem1  22037  ply1scleq  22249  mdetralt  22552  mdetunilem1  22556  lmcvg  23206  iscncl  23213  lmff  23245  cnrmi  23304  cmpcov  23333  fiuncmp  23348  hauscmplem  23350  1stcfb  23389  1stcelcls  23405  restnlly  23426  islly2  23428  lly1stc  23440  kgeni  23481  ptpjpre1  23515  ptbasfi  23525  ptpjopn  23556  dfac14  23562  txtube  23584  cnmpt11  23607  cnmpt21  23615  cnmptkp  23624  cnmptk1p  23629  qtopomap  23662  qtopcmap  23663  flimcf  23926  fclscf  23969  flfcntr  23987  ptcmplem3  23998  tgpt0  24063  tsmsi  24078  tsmsxplem2  24098  tsmsxp  24099  isucn2  24222  ucnima  24224  ucncn  24228  cfiluweak  24238  cuspcvg  24244  imasdsf1olem  24317  lpbl  24447  comet  24457  cfilucfil  24503  cnheiborlem  24909  cnheibor  24910  bndth  24913  nmoleub2lem2  25072  nmoleub3  25075  ipcau2  25190  tcphcphlem1  25191  tcphcphlem2  25192  lmmcvg  25217  cmetcaulem  25244  iscmet3lem1  25247  iscmet3lem2  25248  pjthlem1  25393  pjthlem2  25394  ivthlem1  25408  ivthlem2  25409  ivthlem3  25410  ivth2  25412  ivthle  25413  ivthle2  25414  ivthicc  25415  ovoliunlem1  25459  ovolshftlem1  25466  ovolscalem1  25470  ovolicc2lem3  25476  ovolicc2lem4  25477  ovolicc2  25479  volsup  25513  dyadmbl  25557  vitalilem2  25566  vitalilem3  25567  mbfdm  25583  ismbf3d  25611  cncombf  25615  itg2seq  25699  itg2monolem2  25708  itg2monolem3  25709  itg2mono  25710  iblitg  25725  itgconst  25776  itgfsum  25784  limcvallem  25828  cnlimci  25846  cnmptlimc  25847  dvferm1lem  25944  dvferm1  25945  dvferm2lem  25946  dvferm2  25947  dvlipcn  25955  dvle  25968  lhop1lem  25974  dvfsumge  25984  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  ftc1a  26000  ftc1lem4  26002  itgsubstlem  26011  mdeglt  26026  deg1lt  26058  ply1divex  26098  fta1glem2  26130  fta1g  26131  plyco0  26153  plyeq0lem  26171  dgrcolem2  26236  plydivlem4  26260  plydivex  26261  fta1lem  26271  vieta1lem2  26275  vieta1  26276  tayl0  26325  ulmi  26351  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  mtest  26369  pserulm  26387  efif1olem4  26510  rlimcnp  26931  rlimcnp2  26932  xrlimcnp  26934  scvxcvx  26952  lgamgulmlem5  26999  lgambdd  27003  lgamcvglem  27006  wilthlem2  27035  fsumdvdscom  27151  musumsum  27158  chtub  27179  fsumvma  27180  perfectlem2  27197  dchrelbas3  27205  dchrelbasd  27206  dchrn0  27217  dchrptlem2  27232  lgsval2lem  27274  lgsdirnn0  27311  lgsdinn0  27312  2sqlem10  27395  dchrisumlem1  27456  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrisum0flblem2  27476  dchrisum0flb  27477  dchrisum0lem1b  27482  dchrisum0lem2  27485  2vmadivsumlem  27507  chpdifbndlem1  27520  selberg3lem1  27524  selberg4lem1  27527  pntrsumbnd2  27534  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntibndlem2  27558  pntibndlem3  27559  pntlemn  27567  pntlemj  27570  pntlemi  27571  pntlemo  27574  pntleme  27575  pntlem3  27576  pntlemp  27577  ostth2lem1  27585  ostthlem1  27594  ostth2lem2  27601  ostth3  27605  nosupprefixmo  27668  noinfprefixmo  27669  noinfbnd1lem1  27691  noinfbnd1lem4  27694  noinfbnd2lem1  27698  noinfbnd2  27699  eqcuts3  27800  cofslts  27914  coinitslts  27915  leadds1  27985  addsass  28001  addbdaylem  28013  negsid  28037  mulscom  28135  addsdilem3  28149  addsdilem4  28150  mulsasslem3  28161  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  addonbday  28275  n0fincut  28351  onsfi  28352  bdayfinbndlem1  28463  bdayfinbnd  28465  tglowdim1i  28573  tglowdim2ln  28723  wlkonl1iedg  29737  wlkp1lem7  29751  wlkp1lem8  29752  crctcshwlkn0lem6  29888  eupth2eucrct  30292  eupth2lem3  30311  ubthlem1  30945  ubthlem2  30946  minvecolem3  30951  occllem  31378  pjhthlem1  31466  eqelbid  32549  fnfvor  32687  ofrco  32688  wrdt2ind  33035  mgccole1  33072  mgcmnt2  33075  dfmgc2  33078  fxpgaeq  33251  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  elrgspnlem4  33327  elrgspnsubrunlem2  33330  0nellinds  33451  linds2eq  33462  elrspunidl  33509  prmidl  33521  mxidlmax  33546  ssmxidl  33555  1arithidomlem1  33616  1arithidom  33618  1arithufdlem3  33627  1arithufdlem4  33628  ply1dg1rt  33661  vietalem  33735  lbsdiflsp0  33783  fedgmullem1  33786  fedgmullem2  33787  extdg1id  33823  fldextrspunlsplem  33830  extdgfialglem2  33850  constrsscn  33897  constrconj  33902  zrhcntr  34136  ofcfeqd2  34258  inelpisys  34311  unelldsys  34315  ldgenpisyslem1  34320  mbfmcnvima  34412  signstfvneq0  34729  fsum2dsub  34764  hgt750lemc  34804  hgt750lemd  34805  hgt749d  34806  hgt750lemf  34810  bnj1379  34986  bnj1450  35206  revwlk  35319  subfacp1lem5  35378  cvmlift2lem10  35506  weiunfrlem  36658  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  unblimceq0lem  36706  unblimceq0  36707  unbdqndv2  36711  bj-ismoored  37312  lcmineqlem4  42286  dvle2  42326  aks4d1p9  42342  primrootlekpowne0  42359  aks6d1c1p3  42364  aks6d1c1p4  42365  aks6d1c1p5  42366  aks6d1c1  42370  hashscontpow  42376  aks6d1c2lem3  42380  sticksstones1  42400  aks6d1c6lem1  42424  aks6d1c6lem2  42425  aks6d1c6lem4  42427  aks6d1c7  42438  aks5lem3a  42443  unitscyglem1  42449  unitscyglem2  42450  unitscyglem3  42451  unitscyglem4  42452  exfinfldd  42457  fnwe2lem2  43293  aomclem4  43299  scottelrankd  44488  mnuop123d  44503  mnuprdlem1  44513  mnuprdlem2  44514  eliind  45316  rnmptbd2lem  45492  rnmptbdlem  45499  cvgcau  45734  limclner  45895  climisp  45990  climrescn  45992  climxrrelem  45993  climxrre  45994  liminflelimsuplem  46019  cncfshift  46118  cncfperiod  46123  fperdvper  46163  salunicl  46560  saldifcl  46563  meadjuni  46701  chnerlem1  47126  lubsscl  49205  glbsscl  49206  ipolub  49233  ipoglb  49236  ssccatid  49317  upciclem1  49411  oppcup3lem  49451  oppcthinendcALT  49686  setcthin  49710