Theorem rspcdva 3517

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1601   ∈ wcel 2107  ∀wral 3090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400

This theorem is referenced by:  nvocnv  6811  knatar  6881  grprinvlem  7151  grprinvd  7152  caofref  7202  caofinvl  7203  tfisi  7338  suppssov1  7611  wfrlem17  7716  tfrlem1  7757  tfrlem5  7761  marypha1lem  8629  marypha1  8630  ordtypelem6  8719  ordtypelem7  8720  wemaplem2  8743  oemapvali  8880  cantnflem1c  8883  infxpenlem  9171  acni  9203  dfac9  9295  dfac12lem2  9303  sornom  9436  fin1ai  9452  fin2i  9454  fin23lem11  9476  isfin2-2  9478  fin23lem17  9497  fin23lem39  9509  fin1a2lem13  9571  hsmexlem4  9588  ttukeylem5  9672  ttukeylem6  9673  canth4  9806  pwfseqlem5  9822  winalim2  9855  wununi  9865  wunpw  9866  dedekind  10541  zsupss  12089  uzwo3  12095  seqcl2  13142  seqcl  13144  seqf  13145  seqfveq2  13146  seqfveq  13148  seqshft2  13150  monoord  13154  monoord2  13155  sermono  13156  seqsplit  13157  seqcaopr3  13159  seqid  13169  seqid2  13170  seqhomo  13171  seqz  13172  discr1  13324  discr  13325  hashbclem  13556  wrdind  13848  wrdindOLD  13849  limsupgre  14629  climi  14658  rlimi  14661  rlimclim1  14693  rlimclim  14694  climrlim2  14695  rlimcn1  14736  climcn1  14739  isercoll2  14816  caucvgrlem  14820  caucvgb  14827  iseraltlem2  14830  iseraltlem3  14831  fsumm1  14896  fsum1p  14898  fsumcom2  14919  fsumge1  14942  telfsumo  14947  telfsumo2  14948  fsumparts  14951  o1fsum  14958  isum1p  14986  isumnn0nn  14987  isumrpcl  14988  climcndslem1  14994  climcndslem2  14995  climcnds  14996  cvgrat  15027  mertenslem1  15028  mertens  15030  fprodm1  15109  fprod1p  15110  fprodcom2  15126  prmind2  15814  pcmpt2  16012  prmpwdvds  16023  prmreclem4  16038  prmreclem5  16039  vdwlem1  16100  vdwlem2  16101  vdwlem9  16108  vdwlem10  16109  rami  16134  ramcl  16148  prmodvdslcmf  16166  prmgaplcmlem1  16170  cshwsidrepsw  16210  prdsbasprj  16529  isacs2  16710  acsfiel  16711  catidex  16731  iscatd2  16738  catlid  16740  catrid  16741  subcidcl  16900  funcid  16926  yonedalem4c  17314  yonffthlem  17319  isdrs2  17336  luble  17384  glble  17397  joinle  17411  meetle  17425  poslubmo  17543  posglbmo  17544  acsdrsel  17564  isacs4lem  17565  isacs5lem  17566  acsdrscl  17567  acsficl  17568  mrcmndind  17763  grpidd2  17857  mulgsubcl  17953  issubg4  18008  ghmf1  18084  fislw  18435  efgsdmi  18540  efgsrel  18542  gexexlem  18652  gsumzaddlem  18718  gsummhm2  18736  dprdcntz  18805  dprddisj  18806  dprdss  18826  dprd2dlem2  18837  dprd2da  18839  dpjrid  18859  ablfac1eu  18870  pgpfac1lem1  18871  pgpfaclem2  18879  issrngd  19264  islbs2  19562  lbsextlem4  19569  mplsubglem  19842  mpllsslem  19843  subrgasclcl  19906  mplind  19909  evlslem1  19922  prmirredlem  20248  psgndiflemB  20353  frlmphl  20535  mdetralt  20830  mdetunilem1  20834  lmcvg  21485  iscncl  21492  lmff  21524  cnrmi  21583  cmpcov  21612  fiuncmp  21627  hauscmplem  21629  1stcfb  21668  1stcelcls  21684  restnlly  21705  islly2  21707  lly1stc  21719  kgeni  21760  ptpjpre1  21794  ptbasfi  21804  ptpjopn  21835  dfac14  21841  txtube  21863  cnmpt11  21886  cnmpt21  21894  cnmptkp  21903  cnmptk1p  21908  qtopomap  21941  qtopcmap  21942  flimcf  22205  fclscf  22248  flfcntr  22266  ptcmplem3  22277  tgpt0  22341  tsmsi  22356  tsmsxplem2  22376  tsmsxp  22377  isucn2  22502  ucnima  22504  ucncn  22508  cfiluweak  22518  cuspcvg  22524  imasdsf1olem  22597  lpbl  22727  comet  22737  cfilucfil  22783  cnheiborlem  23172  cnheibor  23173  bndth  23176  nmoleub2lem2  23334  nmoleub3  23337  ipcau2  23451  tcphcphlem1  23452  tcphcphlem2  23453  lmmcvg  23478  cmetcaulem  23505  iscmet3lem1  23508  iscmet3lem2  23509  pjthlem1  23654  pjthlem2  23655  ivthlem1  23666  ivthlem2  23667  ivthlem3  23668  ivth2  23670  ivthle  23671  ivthle2  23672  ivthicc  23673  ovoliunlem1  23717  ovolshftlem1  23724  ovolscalem1  23728  ovolicc2lem3  23734  ovolicc2lem4  23735  ovolicc2  23737  volsup  23771  dyadmbl  23815  vitalilem2  23824  vitalilem3  23825  mbfdm  23841  ismbf3d  23869  cncombf  23873  itg2seq  23957  itg2monolem2  23966  itg2monolem3  23967  itg2mono  23968  iblitg  23983  itgconst  24033  itgfsum  24041  limcvallem  24083  cnlimci  24101  cnmptlimc  24102  dvferm1lem  24195  dvferm1  24196  dvferm2lem  24197  dvferm2  24198  dvlipcn  24205  dvle  24218  lhop1lem  24224  dvfsumge  24233  dvfsumlem2  24238  dvfsumlem3  24239  ftc1a  24248  ftc1lem4  24250  itgsubstlem  24259  mdeglt  24273  deg1lt  24305  ply1divex  24344  fta1glem2  24374  fta1g  24375  plyco0  24396  plyeq0lem  24414  dgrcolem2  24478  plydivlem4  24499  plydivex  24500  fta1lem  24510  vieta1lem2  24514  vieta1  24515  tayl0  24564  ulmi  24588  ulmdvlem1  24602  ulmdvlem3  24604  ulmdv  24605  mtest  24606  pserulm  24624  efif1olem4  24740  rlimcnp  25155  rlimcnp2  25156  xrlimcnp  25158  scvxcvx  25175  lgamgulmlem5  25222  lgambdd  25226  lgamcvglem  25229  wilthlem2  25258  fsumdvdscom  25374  musumsum  25381  chtub  25400  fsumvma  25401  perfectlem2  25418  dchrelbas3  25426  dchrelbasd  25427  dchrn0  25438  dchrptlem2  25453  lgsval2lem  25495  lgsdirnn0  25532  lgsdinn0  25533  2sqlem10  25616  dchrisumlem1  25647  dchrmusum2  25652  dchrvmasumlem2  25656  dchrvmasumlem3  25657  dchrvmasumiflem1  25659  dchrisum0flblem2  25667  dchrisum0flb  25668  dchrisum0lem1b  25673  dchrisum0lem2  25676  2vmadivsumlem  25698  chpdifbndlem1  25711  selberg3lem1  25715  selberg4lem1  25718  pntrsumbnd2  25725  pntrlog2bndlem2  25736  pntrlog2bndlem3  25737  pntrlog2bndlem5  25739  pntrlog2bndlem6  25741  pntibndlem2  25749  pntibndlem3  25750  pntlemn  25758  pntlemj  25761  pntlemi  25762  pntlemo  25765  pntleme  25766  pntlem3  25767  pntlemp  25768  ostth2lem1  25776  ostthlem1  25785  ostth2lem2  25792  ostth3  25796  tglowdim1i  25869  tglowdim2ln  26019  wlkonl1iedg  27029  wlkp1lem7  27047  wlkp1lem8  27048  crctcshwlkn0lem6  27181  eupth2eucrct  27638  eupth2lem3  27657  ubthlem1  28315  ubthlem2  28316  minvecolem3  28321  occllem  28751  pjhthlem1  28839  0nellinds  30442  lbsdiflsp0  30448  inelpisys  30823  unelldsys  30827  ldgenpisyslem1  30832  fsum2dsub  31295  hgt750lemc  31335  hgt750lemd  31336  hgt749d  31337  hgt750lemf  31341  cvmlift2lem10  31901  unblimceq0lem  33087  unblimceq0  33088  unbdqndv2  33092  limclner  40805  climisp  40900  climrescn  40902  climxrrelem  40903  climxrre  40904  cncfshift  41029  cncfperiod  41034  fperdvper  41075  saldifcl  41477