Theorem rspcdva 3612

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

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

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 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060

This theorem is referenced by:  nvocnv  7281  knatar  7356  caofref  7701  caofinvl  7702  tfisi  7850  frxp2  8132  frxp3  8139  suppssov1  8185  fpr3g  8272  fprresex  8297  wfrlem17OLD  8327  tfrlem1  8378  tfrlem5  8382  coflton  8672  cofon1  8673  cofon2  8674  marypha1lem  9430  marypha1  9431  ordtypelem6  9520  ordtypelem7  9521  wemaplem2  9544  oemapvali  9681  cantnflem1c  9684  ttrcltr  9713  ttrclss  9717  dmttrcl  9718  rnttrcl  9719  ttrclselem2  9723  infxpenlem  10010  acni  10042  dfac9  10133  dfac12lem2  10141  sornom  10274  fin1ai  10290  fin2i  10292  fin23lem11  10314  isfin2-2  10316  fin23lem17  10335  fin23lem39  10347  fin1a2lem13  10409  hsmexlem4  10426  ttukeylem5  10510  ttukeylem6  10511  canth4  10644  pwfseqlem5  10660  winalim2  10693  wununi  10703  wunpw  10704  dedekind  11381  zsupss  12925  uzwo3  12931  seqcl2  13990  seqcl  13992  seqf  13993  seqfveq2  13994  seqfveq  13996  seqshft2  13998  monoord  14002  monoord2  14003  sermono  14004  seqsplit  14005  seqcaopr3  14007  seqid  14017  seqid2  14018  seqhomo  14019  seqz  14020  discr1  14206  discr  14207  hashbclem  14415  wrdind  14676  limsupgre  15429  climi  15458  rlimi  15461  rlimclim1  15493  rlimclim  15494  climrlim2  15495  rlimcn1  15536  climcn1  15540  isercoll2  15619  caucvgrlem  15623  caucvgb  15630  iseraltlem2  15633  iseraltlem3  15634  fsumm1  15701  fsum1p  15703  fsumcom2  15724  fsumge1  15747  telfsumo  15752  telfsumo2  15753  fsumparts  15756  o1fsum  15763  isum1p  15791  isumnn0nn  15792  isumrpcl  15793  climcndslem1  15799  climcndslem2  15800  climcnds  15801  cvgrat  15833  mertenslem1  15834  mertens  15836  fprodm1  15915  fprod1p  15916  fprodcom2  15932  prmind2  16626  pcmpt2  16830  prmpwdvds  16841  prmreclem4  16856  prmreclem5  16857  vdwlem1  16918  vdwlem2  16919  vdwlem9  16926  vdwlem10  16927  rami  16952  ramcl  16966  prmodvdslcmf  16984  prmgaplcmlem1  16988  cshwsidrepsw  17031  prdsbasprj  17422  isacs2  17601  acsfiel  17602  catidex  17622  iscatd2  17629  catlid  17631  catrid  17632  subcidcl  17798  funcid  17824  yonedalem4c  18234  yonffthlem  18239  isdrs2  18263  luble  18316  glble  18329  joinle  18343  meetle  18357  poslubmo  18368  posglbmo  18369  acsdrsel  18500  isacs4lem  18501  isacs5lem  18502  acsdrscl  18503  acsficl  18504  lidrideqd  18594  grprinvlem  18598  grpinva  18599  mndind  18745  grpidd2  18898  mulgsubcl  19004  issubg4  19061  ghmf1  19160  fislw  19534  efgsdmi  19641  efgsrel  19643  gexexlem  19761  gsumzaddlem  19830  gsummhm2  19848  dprdcntz  19919  dprddisj  19920  dprdss  19940  dprd2dlem2  19951  dprd2da  19953  dpjrid  19973  ablfac1eu  19984  pgpfac1lem1  19985  pgpfaclem2  19993  lringuplu  20432  issrngd  20612  islbs2  20912  lbsextlem4  20919  prmirredlem  21243  psgndiflemB  21372  frlmphl  21555  mplsubglem  21777  mpllsslem  21778  subrgasclcl  21847  mplind  21850  evlslem1  21864  mdetralt  22330  mdetunilem1  22334  lmcvg  22986  iscncl  22993  lmff  23025  cnrmi  23084  cmpcov  23113  fiuncmp  23128  hauscmplem  23130  1stcfb  23169  1stcelcls  23185  restnlly  23206  islly2  23208  lly1stc  23220  kgeni  23261  ptpjpre1  23295  ptbasfi  23305  ptpjopn  23336  dfac14  23342  txtube  23364  cnmpt11  23387  cnmpt21  23395  cnmptkp  23404  cnmptk1p  23409  qtopomap  23442  qtopcmap  23443  flimcf  23706  fclscf  23749  flfcntr  23767  ptcmplem3  23778  tgpt0  23843  tsmsi  23858  tsmsxplem2  23878  tsmsxp  23879  isucn2  24004  ucnima  24006  ucncn  24010  cfiluweak  24020  cuspcvg  24026  imasdsf1olem  24099  lpbl  24232  comet  24242  cfilucfil  24288  cnheiborlem  24700  cnheibor  24701  bndth  24704  nmoleub2lem2  24863  nmoleub3  24866  ipcau2  24982  tcphcphlem1  24983  tcphcphlem2  24984  lmmcvg  25009  cmetcaulem  25036  iscmet3lem1  25039  iscmet3lem2  25040  pjthlem1  25185  pjthlem2  25186  ivthlem1  25200  ivthlem2  25201  ivthlem3  25202  ivth2  25204  ivthle  25205  ivthle2  25206  ivthicc  25207  ovoliunlem1  25251  ovolshftlem1  25258  ovolscalem1  25262  ovolicc2lem3  25268  ovolicc2lem4  25269  ovolicc2  25271  volsup  25305  dyadmbl  25349  vitalilem2  25358  vitalilem3  25359  mbfdm  25375  ismbf3d  25403  cncombf  25407  itg2seq  25492  itg2monolem2  25501  itg2monolem3  25502  itg2mono  25503  iblitg  25518  itgconst  25568  itgfsum  25576  limcvallem  25620  cnlimci  25638  cnmptlimc  25639  dvferm1lem  25736  dvferm1  25737  dvferm2lem  25738  dvferm2  25739  dvlipcn  25746  dvle  25759  lhop1lem  25765  dvfsumge  25774  dvfsumlem2  25779  dvfsumlem3  25780  ftc1a  25789  ftc1lem4  25791  itgsubstlem  25800  mdeglt  25818  deg1lt  25850  ply1divex  25889  fta1glem2  25919  fta1g  25920  plyco0  25941  plyeq0lem  25959  dgrcolem2  26024  plydivlem4  26045  plydivex  26046  fta1lem  26056  vieta1lem2  26060  vieta1  26061  tayl0  26110  ulmi  26134  ulmdvlem1  26148  ulmdvlem3  26150  ulmdv  26151  mtest  26152  pserulm  26170  efif1olem4  26290  rlimcnp  26706  rlimcnp2  26707  xrlimcnp  26709  scvxcvx  26726  lgamgulmlem5  26773  lgambdd  26777  lgamcvglem  26780  wilthlem2  26809  fsumdvdscom  26925  musumsum  26932  chtub  26951  fsumvma  26952  perfectlem2  26969  dchrelbas3  26977  dchrelbasd  26978  dchrn0  26989  dchrptlem2  27004  lgsval2lem  27046  lgsdirnn0  27083  lgsdinn0  27084  2sqlem10  27167  dchrisumlem1  27228  dchrmusum2  27233  dchrvmasumlem2  27237  dchrvmasumlem3  27238  dchrvmasumiflem1  27240  dchrisum0flblem2  27248  dchrisum0flb  27249  dchrisum0lem1b  27254  dchrisum0lem2  27257  2vmadivsumlem  27279  chpdifbndlem1  27292  selberg3lem1  27296  selberg4lem1  27299  pntrsumbnd2  27306  pntrlog2bndlem2  27317  pntrlog2bndlem3  27318  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntibndlem2  27330  pntibndlem3  27331  pntlemn  27339  pntlemj  27342  pntlemi  27343  pntlemo  27346  pntleme  27347  pntlem3  27348  pntlemp  27349  ostth2lem1  27357  ostthlem1  27366  ostth2lem2  27373  ostth3  27377  nosupprefixmo  27439  noinfprefixmo  27440  noinfbnd1lem1  27462  noinfbnd1lem4  27465  noinfbnd2lem1  27469  noinfbnd2  27470  cofsslt  27643  coinitsslt  27644  sleadd1  27711  addsass  27727  negsid  27754  mulscom  27834  addsdilem3  27847  addsdilem4  27848  mulsasslem3  27859  precsexlem8  27899  precsexlem9  27900  precsexlem11  27902  tglowdim1i  28019  tglowdim2ln  28169  wlkonl1iedg  29189  wlkp1lem7  29203  wlkp1lem8  29204  crctcshwlkn0lem6  29336  eupth2eucrct  29737  eupth2lem3  29756  ubthlem1  30390  ubthlem2  30391  minvecolem3  30396  occllem  30823  pjhthlem1  30911  eqelbid  31982  wrdt2ind  32384  mgccole1  32427  mgcmnt2  32430  dfmgc2  32433  0nellinds  32757  linds2eq  32771  elrspunidl  32820  prmidl  32832  mxidlmax  32855  ssmxidl  32864  ply1scleq  32913  lbsdiflsp0  32999  fedgmullem1  33002  fedgmullem2  33003  extdg1id  33030  ofcfeqd2  33397  inelpisys  33450  unelldsys  33454  ldgenpisyslem1  33459  mbfmcnvima  33552  signstfvneq0  33881  fsum2dsub  33917  hgt750lemc  33957  hgt750lemd  33958  hgt749d  33959  hgt750lemf  33963  bnj1379  34139  bnj1450  34359  revwlk  34413  subfacp1lem5  34473  cvmlift2lem10  34601  gg-dvfsumlem2  35469  unblimceq0lem  35685  unblimceq0  35686  unbdqndv2  35690  bj-ismoored  36291  lcmineqlem4  41203  dvle2  41243  aks4d1p9  41259  sticksstones1  41268  fnwe2lem2  42095  aomclem4  42101  scottelrankd  43308  mnuop123d  43323  mnuprdlem1  43333  mnuprdlem2  43334  eliind  44059  rnmptbd2lem  44250  rnmptbdlem  44257  cvgcau  44499  limclner  44665  climisp  44760  climrescn  44762  climxrrelem  44763  climxrre  44764  cncfshift  44888  cncfperiod  44893  fperdvper  44933  salunicl  45330  saldifcl  45333  meadjuni  45471  lubsscl  47680  glbsscl  47681  ipolub  47700  ipoglb  47703  setcthin  47762