Theorem rspcdva 3565

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052

This theorem is referenced by:  nvocnv  7236  knatar  7312  caofref  7662  caofinvl  7663  tfisi  7810  frxp2  8094  frxp3  8101  suppssov1  8147  suppssov2  8148  fpr3g  8235  fprresex  8260  tfrlem1  8315  tfrlem5  8319  coflton  8607  cofon1  8608  cofon2  8609  marypha1lem  9346  marypha1  9347  ordtypelem6  9438  ordtypelem7  9439  wemaplem2  9462  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  11309  zsupss  12887  uzwo3  12893  seqcl2  13982  seqcl  13984  seqf  13985  seqfveq2  13986  seqfveq  13988  seqshft2  13990  monoord  13994  monoord2  13995  sermono  13996  seqsplit  13997  seqcaopr3  13999  seqid  14009  seqid2  14010  seqhomo  14011  seqz  14012  discr1  14201  discr  14202  hashbclem  14414  wrdind  14684  limsupgre  15443  climi  15472  rlimi  15475  rlimclim1  15507  rlimclim  15508  climrlim2  15509  rlimcn1  15550  climcn1  15554  isercoll2  15631  caucvgrlem  15635  caucvgb  15642  iseraltlem2  15645  iseraltlem3  15646  fsumm1  15713  fsum1p  15715  fsumcom2  15736  fsumge1  15760  telfsumo  15765  telfsumo2  15766  fsumparts  15769  o1fsum  15776  isum1p  15806  isumnn0nn  15807  isumrpcl  15808  climcndslem1  15814  climcndslem2  15815  climcnds  15816  cvgrat  15848  mertenslem1  15849  mertens  15851  fprodm1  15932  fprod1p  15933  fprodcom2  15949  prmind2  16654  pcmpt2  16864  prmpwdvds  16875  prmreclem4  16890  prmreclem5  16891  vdwlem1  16952  vdwlem2  16953  vdwlem9  16960  vdwlem10  16961  rami  16986  ramcl  17000  prmodvdslcmf  17018  prmgaplcmlem1  17022  cshwsidrepsw  17064  prdsbasprj  17435  isacs2  17619  acsfiel  17620  catidex  17640  iscatd2  17647  catlid  17649  catrid  17650  subcidcl  17811  funcid  17837  yonedalem4c  18243  yonffthlem  18248  isdrs2  18272  luble  18323  glble  18336  joinle  18350  meetle  18364  poslubmo  18375  posglbmo  18376  acsdrsel  18509  isacs4lem  18510  isacs5lem  18511  acsdrscl  18512  acsficl  18513  chnltm1  18575  chnub  18588  lidrideqd  18637  grpinvalem  18641  grpinva  18642  mndind  18796  grpidd2  18953  mulgsubcl  19064  issubg4  19121  ghmf1  19221  fislw  19600  efgsdmi  19707  efgsrel  19709  gexexlem  19827  gsumzaddlem  19896  gsummhm2  19914  dprdcntz  19985  dprddisj  19986  dprdss  20006  dprd2dlem2  20017  dprd2da  20019  dpjrid  20039  ablfac1eu  20050  pgpfac1lem1  20051  pgpfaclem2  20059  lringuplu  20521  issrngd  20832  islbs2  21152  lbsextlem4  21159  prmirredlem  21452  psgndiflemB  21580  frlmphl  21761  mplsubglem  21977  mpllsslem  21978  subrgasclcl  22045  mplind  22048  evlslem1  22060  ply1scleq  22270  mdetralt  22573  mdetunilem1  22577  lmcvg  23227  iscncl  23234  lmff  23266  cnrmi  23325  cmpcov  23354  fiuncmp  23369  hauscmplem  23371  1stcfb  23410  1stcelcls  23426  restnlly  23447  islly2  23449  lly1stc  23461  kgeni  23502  ptpjpre1  23536  ptbasfi  23546  ptpjopn  23577  dfac14  23583  txtube  23605  cnmpt11  23628  cnmpt21  23636  cnmptkp  23645  cnmptk1p  23650  qtopomap  23683  qtopcmap  23684  flimcf  23947  fclscf  23990  flfcntr  24008  ptcmplem3  24019  tgpt0  24084  tsmsi  24099  tsmsxplem2  24119  tsmsxp  24120  isucn2  24243  ucnima  24245  ucncn  24249  cfiluweak  24259  cuspcvg  24265  imasdsf1olem  24338  lpbl  24468  comet  24478  cfilucfil  24524  cnheiborlem  24921  cnheibor  24922  bndth  24925  nmoleub2lem2  25083  nmoleub3  25086  ipcau2  25201  tcphcphlem1  25202  tcphcphlem2  25203  lmmcvg  25228  cmetcaulem  25255  iscmet3lem1  25258  iscmet3lem2  25259  pjthlem1  25404  pjthlem2  25405  ivthlem1  25418  ivthlem2  25419  ivthlem3  25420  ivth2  25422  ivthle  25423  ivthle2  25424  ivthicc  25425  ovoliunlem1  25469  ovolshftlem1  25476  ovolscalem1  25480  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2  25489  volsup  25523  dyadmbl  25567  vitalilem2  25576  vitalilem3  25577  mbfdm  25593  ismbf3d  25621  cncombf  25625  itg2seq  25709  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  iblitg  25735  itgconst  25786  itgfsum  25794  limcvallem  25838  cnlimci  25856  cnmptlimc  25857  dvferm1lem  25951  dvferm1  25952  dvferm2lem  25953  dvferm2  25954  dvlipcn  25961  dvle  25974  lhop1lem  25980  dvfsumge  25989  dvfsumlem2  25994  dvfsumlem3  25995  ftc1a  26004  ftc1lem4  26006  itgsubstlem  26015  mdeglt  26030  deg1lt  26062  ply1divex  26102  fta1glem2  26134  fta1g  26135  plyco0  26157  plyeq0lem  26175  dgrcolem2  26239  plydivlem4  26262  plydivex  26263  fta1lem  26273  vieta1lem2  26277  vieta1  26278  tayl0  26327  ulmi  26351  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  mtest  26369  pserulm  26387  efif1olem4  26509  rlimcnp  26929  rlimcnp2  26930  xrlimcnp  26932  scvxcvx  26949  lgamgulmlem5  26996  lgambdd  27000  lgamcvglem  27003  wilthlem2  27032  fsumdvdscom  27148  musumsum  27155  chtub  27175  fsumvma  27176  perfectlem2  27193  dchrelbas3  27201  dchrelbasd  27202  dchrn0  27213  dchrptlem2  27228  lgsval2lem  27270  lgsdirnn0  27307  lgsdinn0  27308  2sqlem10  27391  dchrisumlem1  27452  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrisum0flblem2  27472  dchrisum0flb  27473  dchrisum0lem1b  27478  dchrisum0lem2  27481  2vmadivsumlem  27503  chpdifbndlem1  27516  selberg3lem1  27520  selberg4lem1  27523  pntrsumbnd2  27530  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntibndlem2  27554  pntibndlem3  27555  pntlemn  27563  pntlemj  27566  pntlemi  27567  pntlemo  27570  pntleme  27571  pntlem3  27572  pntlemp  27573  ostth2lem1  27581  ostthlem1  27590  ostth2lem2  27597  ostth3  27601  nosupprefixmo  27664  noinfprefixmo  27665  noinfbnd1lem1  27687  noinfbnd1lem4  27690  noinfbnd2lem1  27694  noinfbnd2  27695  eqcuts3  27796  cofslts  27910  coinitslts  27911  leadds1  27981  addsass  27997  addbdaylem  28009  negsid  28033  mulscom  28131  addsdilem3  28145  addsdilem4  28146  mulsasslem3  28157  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  addonbday  28271  n0fincut  28347  onsfi  28348  bdayfinbndlem1  28459  bdayfinbnd  28461  tglowdim1i  28569  tglowdim2ln  28719  wlkonl1iedg  29732  wlkp1lem7  29746  wlkp1lem8  29747  crctcshwlkn0lem6  29883  eupth2eucrct  30287  eupth2lem3  30306  ubthlem1  30941  ubthlem2  30942  minvecolem3  30947  occllem  31374  pjhthlem1  31462  eqelbid  32544  fnfvor  32682  ofrco  32683  wrdt2ind  33013  mgccole1  33050  mgcmnt2  33053  dfmgc2  33056  fxpgaeq  33230  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  elrgspnlem4  33306  elrgspnsubrunlem2  33309  0nellinds  33430  linds2eq  33441  elrspunidl  33488  prmidl  33500  mxidlmax  33525  ssmxidl  33534  1arithidomlem1  33595  1arithidom  33597  1arithufdlem3  33606  1arithufdlem4  33607  ply1dg1rt  33640  vietalem  33723  lbsdiflsp0  33770  fedgmullem1  33773  fedgmullem2  33774  extdg1id  33810  fldextrspunlsplem  33817  extdgfialglem2  33837  constrsscn  33884  constrconj  33889  zrhcntr  34123  ofcfeqd2  34245  inelpisys  34298  unelldsys  34302  ldgenpisyslem1  34307  mbfmcnvima  34399  signstfvneq0  34716  fsum2dsub  34751  hgt750lemc  34791  hgt750lemd  34792  hgt749d  34793  hgt750lemf  34797  bnj1379  34972  bnj1450  35192  revwlk  35307  subfacp1lem5  35366  cvmlift2lem10  35494  weiunfrlem  36646  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  unblimceq0lem  36766  unblimceq0  36767  unbdqndv2  36771  bj-ismoored  37419  lcmineqlem4  42471  dvle2  42511  aks4d1p9  42527  primrootlekpowne0  42544  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1  42555  hashscontpow  42561  aks6d1c2lem3  42565  sticksstones1  42585  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks6d1c6lem4  42612  aks6d1c7  42623  aks5lem3a  42628  unitscyglem1  42634  unitscyglem2  42635  unitscyglem3  42636  unitscyglem4  42637  exfinfldd  42642  fnwe2lem2  43479  aomclem4  43485  scottelrankd  44674  mnuop123d  44689  mnuprdlem1  44699  mnuprdlem2  44700  eliind  45502  rnmptbd2lem  45677  rnmptbdlem  45684  cvgcau  45918  limclner  46079  climisp  46174  climrescn  46176  climxrrelem  46177  climxrre  46178  liminflelimsuplem  46203  cncfshift  46302  cncfperiod  46307  fperdvper  46347  salunicl  46744  saldifcl  46747  meadjuni  46885  chnerlem1  47312  lubsscl  49435  glbsscl  49436  ipolub  49463  ipoglb  49466  ssccatid  49547  upciclem1  49641  oppcup3lem  49681  oppcthinendcALT  49916  setcthin  49940