Theorem rspcdva 3567

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ∈ wcel 2104  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3063

This theorem is referenced by:  nvocnv  7185  knatar  7260  caofref  7594  caofinvl  7595  tfisi  7737  suppssov1  8045  fpr3g  8132  fprresex  8157  wfrlem17OLD  8187  tfrlem1  8238  tfrlem5  8242  marypha1lem  9236  marypha1  9237  ordtypelem6  9326  ordtypelem7  9327  wemaplem2  9350  oemapvali  9486  cantnflem1c  9489  ttrcltr  9518  ttrclss  9522  dmttrcl  9523  rnttrcl  9524  ttrclselem2  9528  infxpenlem  9815  acni  9847  dfac9  9938  dfac12lem2  9946  sornom  10079  fin1ai  10095  fin2i  10097  fin23lem11  10119  isfin2-2  10121  fin23lem17  10140  fin23lem39  10152  fin1a2lem13  10214  hsmexlem4  10231  ttukeylem5  10315  ttukeylem6  10316  canth4  10449  pwfseqlem5  10465  winalim2  10498  wununi  10508  wunpw  10509  dedekind  11184  zsupss  12723  uzwo3  12729  seqcl2  13787  seqcl  13789  seqf  13790  seqfveq2  13791  seqfveq  13793  seqshft2  13795  monoord  13799  monoord2  13800  sermono  13801  seqsplit  13802  seqcaopr3  13804  seqid  13814  seqid2  13815  seqhomo  13816  seqz  13817  discr1  14000  discr  14001  hashbclem  14209  wrdind  14480  limsupgre  15235  climi  15264  rlimi  15267  rlimclim1  15299  rlimclim  15300  climrlim2  15301  rlimcn1  15342  climcn1  15346  isercoll2  15425  caucvgrlem  15429  caucvgb  15436  iseraltlem2  15439  iseraltlem3  15440  fsumm1  15508  fsum1p  15510  fsumcom2  15531  fsumge1  15554  telfsumo  15559  telfsumo2  15560  fsumparts  15563  o1fsum  15570  isum1p  15598  isumnn0nn  15599  isumrpcl  15600  climcndslem1  15606  climcndslem2  15607  climcnds  15608  cvgrat  15640  mertenslem1  15641  mertens  15643  fprodm1  15722  fprod1p  15723  fprodcom2  15739  prmind2  16435  pcmpt2  16639  prmpwdvds  16650  prmreclem4  16665  prmreclem5  16666  vdwlem1  16727  vdwlem2  16728  vdwlem9  16735  vdwlem10  16736  rami  16761  ramcl  16775  prmodvdslcmf  16793  prmgaplcmlem1  16797  cshwsidrepsw  16840  prdsbasprj  17228  isacs2  17407  acsfiel  17408  catidex  17428  iscatd2  17435  catlid  17437  catrid  17438  subcidcl  17604  funcid  17630  yonedalem4c  18040  yonffthlem  18045  isdrs2  18069  luble  18122  glble  18135  joinle  18149  meetle  18163  poslubmo  18174  posglbmo  18175  acsdrsel  18306  isacs4lem  18307  isacs5lem  18308  acsdrscl  18309  acsficl  18310  lidrideqd  18398  grprinvlem  18402  grprinvd  18403  mndind  18511  grpidd2  18662  mulgsubcl  18763  issubg4  18819  ghmf1  18908  fislw  19275  efgsdmi  19383  efgsrel  19385  gexexlem  19498  gsumzaddlem  19567  gsummhm2  19585  dprdcntz  19656  dprddisj  19657  dprdss  19677  dprd2dlem2  19688  dprd2da  19690  dpjrid  19710  ablfac1eu  19721  pgpfac1lem1  19722  pgpfaclem2  19730  issrngd  20166  islbs2  20461  lbsextlem4  20468  prmirredlem  20739  psgndiflemB  20850  frlmphl  21033  mplsubglem  21250  mpllsslem  21251  subrgasclcl  21320  mplind  21323  evlslem1  21337  mdetralt  21802  mdetunilem1  21806  lmcvg  22458  iscncl  22465  lmff  22497  cnrmi  22556  cmpcov  22585  fiuncmp  22600  hauscmplem  22602  1stcfb  22641  1stcelcls  22657  restnlly  22678  islly2  22680  lly1stc  22692  kgeni  22733  ptpjpre1  22767  ptbasfi  22777  ptpjopn  22808  dfac14  22814  txtube  22836  cnmpt11  22859  cnmpt21  22867  cnmptkp  22876  cnmptk1p  22881  qtopomap  22914  qtopcmap  22915  flimcf  23178  fclscf  23221  flfcntr  23239  ptcmplem3  23250  tgpt0  23315  tsmsi  23330  tsmsxplem2  23350  tsmsxp  23351  isucn2  23476  ucnima  23478  ucncn  23482  cfiluweak  23492  cuspcvg  23498  imasdsf1olem  23571  lpbl  23704  comet  23714  cfilucfil  23760  cnheiborlem  24162  cnheibor  24163  bndth  24166  nmoleub2lem2  24324  nmoleub3  24327  ipcau2  24443  tcphcphlem1  24444  tcphcphlem2  24445  lmmcvg  24470  cmetcaulem  24497  iscmet3lem1  24500  iscmet3lem2  24501  pjthlem1  24646  pjthlem2  24647  ivthlem1  24660  ivthlem2  24661  ivthlem3  24662  ivth2  24664  ivthle  24665  ivthle2  24666  ivthicc  24667  ovoliunlem1  24711  ovolshftlem1  24718  ovolscalem1  24722  ovolicc2lem3  24728  ovolicc2lem4  24729  ovolicc2  24731  volsup  24765  dyadmbl  24809  vitalilem2  24818  vitalilem3  24819  mbfdm  24835  ismbf3d  24863  cncombf  24867  itg2seq  24952  itg2monolem2  24961  itg2monolem3  24962  itg2mono  24963  iblitg  24978  itgconst  25028  itgfsum  25036  limcvallem  25080  cnlimci  25098  cnmptlimc  25099  dvferm1lem  25193  dvferm1  25194  dvferm2lem  25195  dvferm2  25196  dvlipcn  25203  dvle  25216  lhop1lem  25222  dvfsumge  25231  dvfsumlem2  25236  dvfsumlem3  25237  ftc1a  25246  ftc1lem4  25248  itgsubstlem  25257  mdeglt  25275  deg1lt  25307  ply1divex  25346  fta1glem2  25376  fta1g  25377  plyco0  25398  plyeq0lem  25416  dgrcolem2  25480  plydivlem4  25501  plydivex  25502  fta1lem  25512  vieta1lem2  25516  vieta1  25517  tayl0  25566  ulmi  25590  ulmdvlem1  25604  ulmdvlem3  25606  ulmdv  25607  mtest  25608  pserulm  25626  efif1olem4  25746  rlimcnp  26160  rlimcnp2  26161  xrlimcnp  26163  scvxcvx  26180  lgamgulmlem5  26227  lgambdd  26231  lgamcvglem  26234  wilthlem2  26263  fsumdvdscom  26379  musumsum  26386  chtub  26405  fsumvma  26406  perfectlem2  26423  dchrelbas3  26431  dchrelbasd  26432  dchrn0  26443  dchrptlem2  26458  lgsval2lem  26500  lgsdirnn0  26537  lgsdinn0  26538  2sqlem10  26621  dchrisumlem1  26682  dchrmusum2  26687  dchrvmasumlem2  26691  dchrvmasumlem3  26692  dchrvmasumiflem1  26694  dchrisum0flblem2  26702  dchrisum0flb  26703  dchrisum0lem1b  26708  dchrisum0lem2  26711  2vmadivsumlem  26733  chpdifbndlem1  26746  selberg3lem1  26750  selberg4lem1  26753  pntrsumbnd2  26760  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem5  26774  pntrlog2bndlem6  26776  pntibndlem2  26784  pntibndlem3  26785  pntlemn  26793  pntlemj  26796  pntlemi  26797  pntlemo  26800  pntleme  26801  pntlem3  26802  pntlemp  26803  ostth2lem1  26811  ostthlem1  26820  ostth2lem2  26827  ostth3  26831  tglowdim1i  26907  tglowdim2ln  27057  wlkonl1iedg  28078  wlkp1lem7  28092  wlkp1lem8  28093  crctcshwlkn0lem6  28225  eupth2eucrct  28626  eupth2lem3  28645  ubthlem1  29277  ubthlem2  29278  minvecolem3  29283  occllem  29710  pjhthlem1  29798  wrdt2ind  31270  mgccole1  31313  mgcmnt2  31316  dfmgc2  31319  0nellinds  31611  linds2eq  31620  elrspunidl  31651  prmidl  31660  mxidlmax  31682  ssmxidl  31687  ply1scleq  31713  lbsdiflsp0  31752  fedgmullem1  31755  fedgmullem2  31756  extdg1id  31783  ofcfeqd2  32114  inelpisys  32167  unelldsys  32171  ldgenpisyslem1  32176  mbfmcnvima  32269  signstfvneq0  32596  fsum2dsub  32632  hgt750lemc  32672  hgt750lemd  32673  hgt749d  32674  hgt750lemf  32678  bnj1379  32855  bnj1450  33075  revwlk  33131  subfacp1lem5  33191  cvmlift2lem10  33319  frxp2  33836  frxp3  33842  nosupprefixmo  33948  noinfprefixmo  33949  noinfbnd1lem1  33971  noinfbnd1lem4  33974  noinfbnd2lem1  33978  noinfbnd2  33979  cofsslt  34133  coinitsslt  34134  unblimceq0lem  34731  unblimceq0  34732  unbdqndv2  34736  bj-ismoored  35322  lcmineqlem4  40082  dvle2  40122  aks4d1p9  40138  sticksstones1  40144  fnwe2lem2  40914  aomclem4  40920  scottelrankd  41903  mnuop123d  41918  mnuprdlem1  41928  mnuprdlem2  41929  eliind  42657  rnmptbd2lem  42839  rnmptbdlem  42846  limclner  43241  climisp  43336  climrescn  43338  climxrrelem  43339  climxrre  43340  cncfshift  43464  cncfperiod  43469  fperdvper  43509  salunicl  43906  saldifcl  43909  meadjuni  44045  lubsscl  46312  glbsscl  46313  ipolub  46332  ipoglb  46335  setcthin  46394