Theorem rspcdva 2818

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ∈ wcel 2125  ∀wral 2432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-v 2711

This theorem is referenced by:  frirrg  4305  wetriext  4530  tfisi  4540  omsinds  4575  grprinvlem  6005  grprinvd  6006  suppssov1  6019  caofref  6043  caofinvl  6044  oprssdmm  6109  tfrlem1  6245  tfrlem5  6251  tfr1onlemsucfn  6277  tfr1onlemsucaccv  6278  tfr1onlembxssdm  6280  tfr1onlembfn  6281  tfr1onlemaccex  6285  tfr1onlemres  6286  tfrcllemsucfn  6290  tfrcllemsucaccv  6291  tfrcllembxssdm  6293  tfrcllembfn  6294  tfrcllemaccex  6298  tfrcllemres  6299  tfrcl  6301  rdgon  6323  frecabcl  6336  undifdcss  6856  ctssdclemn0  7040  ctssdc  7043  enomnilem  7060  fodju0  7069  fodjuomnilemres  7070  ismkvnex  7077  fodjumkvlemres  7081  enmkvlem  7083  enwomnilem  7091  exmidaclem  7122  exmidontriimlem4  7138  cc2lem  7165  cc3  7167  prltlu  7386  cauappcvgprlemm  7544  caucvgprlemm  7567  caucvgprprlemml  7593  suplocexprlemmu  7617  suplocexprlemdisj  7619  suplocexprlemloc  7620  suplocexprlemub  7622  caucvgsrlemgt1  7694  caucvgsr  7701  suplocsrlemb  7705  suplocsrlempr  7706  suplocsrlem  7707  axcaucvglemcau  7797  axcaucvglemres  7798  axpre-suploclemres  7800  exbtwnzlemstep  10125  apbtwnz  10151  frecuzrdgsuc  10291  frecuzrdgg  10293  frecuzrdgsuctlem  10300  uzsinds  10319  iseqovex  10333  seq3val  10335  seqvalcd  10336  seq3-1  10337  seqf  10338  seq3p1  10339  seqovcd  10340  seqp1cd  10343  seq3clss  10344  seq3fveq2  10346  seq3fveq  10348  seq3feq  10349  seq3shft2  10350  monoord  10353  monoord2  10354  ser3mono  10355  seq3split  10356  seq3caopr3  10358  iseqf1olemkle  10361  iseqf1olemklt  10362  iseqf1olemjpcl  10372  iseqf1olemqpcl  10373  iseqf1olemfvp  10374  seq3f1olemqsumkj  10375  seq3f1olemqsum  10377  seq3f1oleml  10380  seq3f1o  10381  seq3id3  10384  seq3id  10385  seq3id2  10386  seq3homo  10387  seq3z  10388  ser3ge0  10394  zfz1isolemiso  10687  seq3shft  10715  cvg1nlemcau  10861  cvg1nlemres  10862  recvguniq  10872  resqrexlemgt0  10897  resqrexlemoverl  10898  resqrexlemglsq  10899  climi  11161  climcn1  11182  serf0  11226  fsum3cvg  11252  summodclem2  11256  summodc  11257  fsum3  11261  isumz  11263  fsumf1o  11264  isumss  11265  fisumss  11266  isumss2  11267  fsum3cvg2  11268  fsum3cvg3  11270  fsum3ser  11271  fsumsplit  11281  fsumm1  11290  fsum1p  11292  fisumcom2  11312  fsumge1  11335  telfsumo  11340  telfsumo2  11341  fsumparts  11344  isumshft  11364  isum1p  11366  isumnn0nn  11367  isumrpcl  11368  cvgratnnlemnexp  11398  cvgratnnlemmn  11399  cvgratnnlemseq  11400  cvgratnnlemabsle  11401  cvgratnnlemfm  11403  cvgratnnlemrate  11404  cvgratnn  11405  cvgratz  11406  mertenslemi1  11409  mertenslem2  11410  mertensabs  11411  fproddccvg  11446  prodmodclem2a  11450  prodmodc  11452  zproddc  11453  fprodseq  11457  prod1dc  11460  fprodf1o  11462  prodssdc  11463  fprodssdc  11464  fprodm1  11472  fprod1p  11473  fprodcom2fi  11500  bezoutlemmain  11853  bezoutlemex  11856  bezoutlemzz  11857  bezoutlemmo  11861  bezoutlemle  11863  bezoutlemsup  11864  prmind2  11968  ennnfonelemk  12080  ennnfonelemex  12094  ennnfonelemnn0  12102  ctinfomlemom  12107  ctiunctlemudc  12117  icnpimaex  12550  lmcvg  12556  lmff  12588  cnmpt11  12622  cnmpt21  12630  comet  12838  dedekindeulemuub  12934  dedekindeulemloc  12936  dedekindeulemlu  12938  dedekindeulemeu  12939  suplociccreex  12941  suplociccex  12942  dedekindicclemuub  12943  dedekindicclemloc  12945  dedekindicclemlu  12947  dedekindicclemeu  12948  dedekindicc  12950  ivthinclemlopn  12953  ivthinclemlr  12954  ivthinclemuopn  12955  ivthinclemur  12956  ivthinclemdisj  12957  ivthinclemloc  12958  ivthinc  12960  ivthdec  12961  limcimolemlt  12972  limcimo  12973  cnplimclemr  12977  cnlimci  12981  cnmptlimc  12982  limccnpcntop  12983  limccoap  12986  dvcoapbr  13010  eflt  13035  sin0pilem2  13042  pilem3  13043  subctctexmid  13512  pw1nct  13514  nnsf  13517  nninfalllemn  13520  nninfalllem1  13521  nninfsellemeqinf  13529  isomninnlem  13542  trilpolemlt1  13553  trirec0  13556  apdiff  13560  iswomninnlem  13561  ismkvnnlem  13564  redcwlpolemeq1  13566  redc0  13569  reap0  13570  dceqnconst  13571  dcapnconst  13572  nconstwlpolem0  13574  nconstwlpolem  13576