Theorem rspcdva 3573

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  ∀wral 3106

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111

This theorem is referenced by:  nvocnv  7016  knatar  7089  caofref  7415  caofinvl  7416  tfisi  7553  suppssov1  7845  wfrlem17  7954  tfrlem1  7995  tfrlem5  7999  marypha1lem  8881  marypha1  8882  ordtypelem6  8971  ordtypelem7  8972  wemaplem2  8995  oemapvali  9131  cantnflem1c  9134  infxpenlem  9424  acni  9456  dfac9  9547  dfac12lem2  9555  sornom  9688  fin1ai  9704  fin2i  9706  fin23lem11  9728  isfin2-2  9730  fin23lem17  9749  fin23lem39  9761  fin1a2lem13  9823  hsmexlem4  9840  ttukeylem5  9924  ttukeylem6  9925  canth4  10058  pwfseqlem5  10074  winalim2  10107  wununi  10117  wunpw  10118  dedekind  10792  zsupss  12325  uzwo3  12331  seqcl2  13384  seqcl  13386  seqf  13387  seqfveq2  13388  seqfveq  13390  seqshft2  13392  monoord  13396  monoord2  13397  sermono  13398  seqsplit  13399  seqcaopr3  13401  seqid  13411  seqid2  13412  seqhomo  13413  seqz  13414  discr1  13596  discr  13597  hashbclem  13806  wrdind  14075  limsupgre  14830  climi  14859  rlimi  14862  rlimclim1  14894  rlimclim  14895  climrlim2  14896  rlimcn1  14937  climcn1  14940  isercoll2  15017  caucvgrlem  15021  caucvgb  15028  iseraltlem2  15031  iseraltlem3  15032  fsumm1  15098  fsum1p  15100  fsumcom2  15121  fsumge1  15144  telfsumo  15149  telfsumo2  15150  fsumparts  15153  o1fsum  15160  isum1p  15188  isumnn0nn  15189  isumrpcl  15190  climcndslem1  15196  climcndslem2  15197  climcnds  15198  cvgrat  15231  mertenslem1  15232  mertens  15234  fprodm1  15313  fprod1p  15314  fprodcom2  15330  prmind2  16019  pcmpt2  16219  prmpwdvds  16230  prmreclem4  16245  prmreclem5  16246  vdwlem1  16307  vdwlem2  16308  vdwlem9  16315  vdwlem10  16316  rami  16341  ramcl  16355  prmodvdslcmf  16373  prmgaplcmlem1  16377  cshwsidrepsw  16419  prdsbasprj  16737  isacs2  16916  acsfiel  16917  catidex  16937  iscatd2  16944  catlid  16946  catrid  16947  subcidcl  17106  funcid  17132  yonedalem4c  17519  yonffthlem  17524  isdrs2  17541  luble  17589  glble  17602  joinle  17616  meetle  17630  poslubmo  17748  posglbmo  17749  acsdrsel  17769  isacs4lem  17770  isacs5lem  17771  acsdrscl  17772  acsficl  17773  lidrideqd  17871  grprinvlem  17875  grprinvd  17876  mndind  17984  grpidd2  18133  mulgsubcl  18234  issubg4  18290  ghmf1  18379  fislw  18742  efgsdmi  18850  efgsrel  18852  gexexlem  18965  gsumzaddlem  19034  gsummhm2  19052  dprdcntz  19123  dprddisj  19124  dprdss  19144  dprd2dlem2  19155  dprd2da  19157  dpjrid  19177  ablfac1eu  19188  pgpfac1lem1  19189  pgpfaclem2  19197  issrngd  19625  islbs2  19919  lbsextlem4  19926  prmirredlem  20186  psgndiflemB  20289  frlmphl  20470  mplsubglem  20672  mpllsslem  20673  subrgasclcl  20738  mplind  20741  evlslem1  20754  mdetralt  21213  mdetunilem1  21217  lmcvg  21867  iscncl  21874  lmff  21906  cnrmi  21965  cmpcov  21994  fiuncmp  22009  hauscmplem  22011  1stcfb  22050  1stcelcls  22066  restnlly  22087  islly2  22089  lly1stc  22101  kgeni  22142  ptpjpre1  22176  ptbasfi  22186  ptpjopn  22217  dfac14  22223  txtube  22245  cnmpt11  22268  cnmpt21  22276  cnmptkp  22285  cnmptk1p  22290  qtopomap  22323  qtopcmap  22324  flimcf  22587  fclscf  22630  flfcntr  22648  ptcmplem3  22659  tgpt0  22724  tsmsi  22739  tsmsxplem2  22759  tsmsxp  22760  isucn2  22885  ucnima  22887  ucncn  22891  cfiluweak  22901  cuspcvg  22907  imasdsf1olem  22980  lpbl  23110  comet  23120  cfilucfil  23166  cnheiborlem  23559  cnheibor  23560  bndth  23563  nmoleub2lem2  23721  nmoleub3  23724  ipcau2  23838  tcphcphlem1  23839  tcphcphlem2  23840  lmmcvg  23865  cmetcaulem  23892  iscmet3lem1  23895  iscmet3lem2  23896  pjthlem1  24041  pjthlem2  24042  ivthlem1  24055  ivthlem2  24056  ivthlem3  24057  ivth2  24059  ivthle  24060  ivthle2  24061  ivthicc  24062  ovoliunlem1  24106  ovolshftlem1  24113  ovolscalem1  24117  ovolicc2lem3  24123  ovolicc2lem4  24124  ovolicc2  24126  volsup  24160  dyadmbl  24204  vitalilem2  24213  vitalilem3  24214  mbfdm  24230  ismbf3d  24258  cncombf  24262  itg2seq  24346  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  iblitg  24372  itgconst  24422  itgfsum  24430  limcvallem  24474  cnlimci  24492  cnmptlimc  24493  dvferm1lem  24587  dvferm1  24588  dvferm2lem  24589  dvferm2  24590  dvlipcn  24597  dvle  24610  lhop1lem  24616  dvfsumge  24625  dvfsumlem2  24630  dvfsumlem3  24631  ftc1a  24640  ftc1lem4  24642  itgsubstlem  24651  mdeglt  24666  deg1lt  24698  ply1divex  24737  fta1glem2  24767  fta1g  24768  plyco0  24789  plyeq0lem  24807  dgrcolem2  24871  plydivlem4  24892  plydivex  24893  fta1lem  24903  vieta1lem2  24907  vieta1  24908  tayl0  24957  ulmi  24981  ulmdvlem1  24995  ulmdvlem3  24997  ulmdv  24998  mtest  24999  pserulm  25017  efif1olem4  25137  rlimcnp  25551  rlimcnp2  25552  xrlimcnp  25554  scvxcvx  25571  lgamgulmlem5  25618  lgambdd  25622  lgamcvglem  25625  wilthlem2  25654  fsumdvdscom  25770  musumsum  25777  chtub  25796  fsumvma  25797  perfectlem2  25814  dchrelbas3  25822  dchrelbasd  25823  dchrn0  25834  dchrptlem2  25849  lgsval2lem  25891  lgsdirnn0  25928  lgsdinn0  25929  2sqlem10  26012  dchrisumlem1  26073  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrisum0flblem2  26093  dchrisum0flb  26094  dchrisum0lem1b  26099  dchrisum0lem2  26102  2vmadivsumlem  26124  chpdifbndlem1  26137  selberg3lem1  26141  selberg4lem1  26144  pntrsumbnd2  26151  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntibndlem2  26175  pntibndlem3  26176  pntlemn  26184  pntlemj  26187  pntlemi  26188  pntlemo  26191  pntleme  26192  pntlem3  26193  pntlemp  26194  ostth2lem1  26202  ostthlem1  26211  ostth2lem2  26218  ostth3  26222  tglowdim1i  26295  tglowdim2ln  26445  wlkonl1iedg  27455  wlkp1lem7  27469  wlkp1lem8  27470  crctcshwlkn0lem6  27601  eupth2eucrct  28002  eupth2lem3  28021  ubthlem1  28653  ubthlem2  28654  minvecolem3  28659  occllem  29086  pjhthlem1  29174  wrdt2ind  30653  mgccole1  30698  mcgmnt2  30701  dfmgc2  30704  0nellinds  30986  linds2eq  30995  elrspunidl  31014  prmidl  31023  mxidlmax  31045  ssmxidl  31050  lbsdiflsp0  31110  fedgmullem1  31113  fedgmullem2  31114  extdg1id  31141  ofcfeqd2  31470  inelpisys  31523  unelldsys  31527  ldgenpisyslem1  31532  mbfmcnvima  31625  signstfvneq0  31952  fsum2dsub  31988  hgt750lemc  32028  hgt750lemd  32029  hgt749d  32030  hgt750lemf  32034  bnj1379  32212  bnj1450  32432  revwlk  32484  cvmlift2lem10  32672  fpr3g  33235  unblimceq0lem  33958  unblimceq0  33959  unbdqndv2  33963  bj-ismoored  34522  lcmineqlem4  39320  fnwe2lem2  39995  aomclem4  40001  scottelrankd  40955  mnuop123d  40970  mnuprdlem1  40980  mnuprdlem2  40981  eliind  41705  rnmptbd2lem  41886  rnmptbdlem  41893  limclner  42293  climisp  42388  climrescn  42390  climxrrelem  42391  climxrre  42392  cncfshift  42516  cncfperiod  42521  fperdvper  42561  salunicl  42958  saldifcl  42961  meadjuni  43096