Theorem rspcdva 2789

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1331   ∈ wcel 1480  ∀wral 2414

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-v 2683

This theorem is referenced by:  frirrg  4267  wetriext  4486  tfisi  4496  omsinds  4530  grprinvlem  5958  grprinvd  5959  suppssov1  5972  caofref  5996  caofinvl  5997  oprssdmm  6062  tfrlem1  6198  tfrlem5  6204  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  tfrcllemsucfn  6243  tfrcllemsucaccv  6244  tfrcllembxssdm  6246  tfrcllembfn  6247  tfrcllemaccex  6251  tfrcllemres  6252  tfrcl  6254  rdgon  6276  frecabcl  6289  undifdcss  6804  ctssdclemn0  6988  ctssdc  6991  enomnilem  7003  fodju0  7012  fodjuomnilemres  7013  ismkvnex  7022  fodjumkvlemres  7026  exmidaclem  7057  prltlu  7288  cauappcvgprlemm  7446  caucvgprlemm  7469  caucvgprprlemml  7495  suplocexprlemmu  7519  suplocexprlemdisj  7521  suplocexprlemloc  7522  suplocexprlemub  7524  caucvgsrlemgt1  7596  caucvgsr  7603  suplocsrlemb  7607  suplocsrlempr  7608  suplocsrlem  7609  axcaucvglemcau  7699  axcaucvglemres  7700  axpre-suploclemres  7702  exbtwnzlemstep  10018  apbtwnz  10040  frecuzrdgsuc  10180  frecuzrdgg  10182  frecuzrdgsuctlem  10189  uzsinds  10208  iseqovex  10222  seq3val  10224  seqvalcd  10225  seq3-1  10226  seqf  10227  seq3p1  10228  seqovcd  10229  seqp1cd  10232  seq3clss  10233  seq3fveq2  10235  seq3fveq  10237  seq3feq  10238  seq3shft2  10239  monoord  10242  monoord2  10243  ser3mono  10244  seq3split  10245  seq3caopr3  10247  iseqf1olemkle  10250  iseqf1olemklt  10251  iseqf1olemjpcl  10261  iseqf1olemqpcl  10262  iseqf1olemfvp  10263  seq3f1olemqsumkj  10264  seq3f1olemqsum  10266  seq3f1oleml  10269  seq3f1o  10270  seq3id3  10273  seq3id  10274  seq3id2  10275  seq3homo  10276  seq3z  10277  ser3ge0  10283  zfz1isolemiso  10575  seq3shft  10603  cvg1nlemcau  10749  cvg1nlemres  10750  recvguniq  10760  resqrexlemgt0  10785  resqrexlemoverl  10786  resqrexlemglsq  10787  climi  11049  climcn1  11070  serf0  11114  fsum3cvg  11139  summodclem2  11144  summodc  11145  fsum3  11149  isumz  11151  fsumf1o  11152  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsum3cvg3  11158  fsum3ser  11159  fsumsplit  11169  fsumm1  11178  fsum1p  11180  fisumcom2  11200  fsumge1  11223  telfsumo  11228  telfsumo2  11229  fsumparts  11232  isumshft  11252  isum1p  11254  isumnn0nn  11255  isumrpcl  11256  cvgratnnlemnexp  11286  cvgratnnlemmn  11287  cvgratnnlemseq  11288  cvgratnnlemabsle  11289  cvgratnnlemfm  11291  cvgratnnlemrate  11292  cvgratnn  11293  cvgratz  11294  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  fproddccvg  11334  bezoutlemmain  11675  bezoutlemex  11678  bezoutlemzz  11679  bezoutlemmo  11683  bezoutlemle  11685  bezoutlemsup  11686  prmind2  11790  ennnfonelemk  11902  ennnfonelemex  11916  ennnfonelemnn0  11924  ctinfomlemom  11929  ctiunctlemudc  11939  icnpimaex  12369  lmcvg  12375  lmff  12407  cnmpt11  12441  cnmpt21  12449  comet  12657  dedekindeulemuub  12753  dedekindeulemloc  12755  dedekindeulemlu  12757  dedekindeulemeu  12758  suplociccreex  12760  suplociccex  12761  dedekindicclemuub  12762  dedekindicclemloc  12764  dedekindicclemlu  12766  dedekindicclemeu  12767  dedekindicc  12769  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemdisj  12776  ivthinclemloc  12777  ivthinc  12779  ivthdec  12780  limcimolemlt  12791  limcimo  12792  cnplimclemr  12796  cnlimci  12800  cnmptlimc  12801  limccnpcntop  12802  limccoap  12805  dvcoapbr  12829  sin0pilem2  12852  pilem3  12853  subctctexmid  13185  nnsf  13188  nninfalllemn  13191  nninfalllem1  13192  nninfsellemeqinf  13201  isomninnlem  13214  trilpolemlt1  13223