ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rspcdva GIF version

Theorem rspcdva 2766
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
StepHypRef Expression
1 rspcdva.3 . 2 (𝜑𝐶𝐴)
2 rspcdva.2 . 2 (𝜑 → ∀𝑥𝐴 𝜓)
3 rspcdva.1 . . 3 (𝑥 = 𝐶 → (𝜓𝜒))
43rspcv 2757 . 2 (𝐶𝐴 → (∀𝑥𝐴 𝜓𝜒))
51, 2, 4sylc 62 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1314  wcel 1463  wral 2391
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 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-v 2660
This theorem is referenced by:  frirrg  4240  wetriext  4459  tfisi  4469  omsinds  4503  grprinvlem  5931  grprinvd  5932  suppssov1  5945  caofref  5969  caofinvl  5970  oprssdmm  6035  tfrlem1  6171  tfrlem5  6177  tfr1onlemsucfn  6203  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemaccex  6211  tfr1onlemres  6212  tfrcllemsucfn  6216  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemaccex  6224  tfrcllemres  6225  tfrcl  6227  rdgon  6249  frecabcl  6262  undifdcss  6777  ctssdclemn0  6961  ctssdc  6964  enomnilem  6976  fodju0  6985  fodjuomnilemres  6986  ismkvnex  6995  fodjumkvlemres  6999  exmidaclem  7028  prltlu  7259  cauappcvgprlemm  7417  caucvgprlemm  7440  caucvgprprlemml  7466  suplocexprlemmu  7490  suplocexprlemdisj  7492  suplocexprlemloc  7493  suplocexprlemub  7495  caucvgsrlemgt1  7567  caucvgsr  7574  suplocsrlemb  7578  suplocsrlempr  7579  suplocsrlem  7580  axcaucvglemcau  7670  axcaucvglemres  7671  axpre-suploclemres  7673  exbtwnzlemstep  9976  apbtwnz  9998  frecuzrdgsuc  10138  frecuzrdgg  10140  frecuzrdgsuctlem  10147  uzsinds  10166  iseqovex  10180  seq3val  10182  seqvalcd  10183  seq3-1  10184  seqf  10185  seq3p1  10186  seqovcd  10187  seqp1cd  10190  seq3clss  10191  seq3fveq2  10193  seq3fveq  10195  seq3feq  10196  seq3shft2  10197  monoord  10200  monoord2  10201  ser3mono  10202  seq3split  10203  seq3caopr3  10205  iseqf1olemkle  10208  iseqf1olemklt  10209  iseqf1olemjpcl  10219  iseqf1olemqpcl  10220  iseqf1olemfvp  10221  seq3f1olemqsumkj  10222  seq3f1olemqsum  10224  seq3f1oleml  10227  seq3f1o  10228  seq3id3  10231  seq3id  10232  seq3id2  10233  seq3homo  10234  seq3z  10235  ser3ge0  10241  zfz1isolemiso  10533  seq3shft  10561  cvg1nlemcau  10707  cvg1nlemres  10708  recvguniq  10718  resqrexlemgt0  10743  resqrexlemoverl  10744  resqrexlemglsq  10745  climi  11007  climcn1  11028  serf0  11072  fsum3cvg  11097  summodclem2  11102  summodc  11103  fsum3  11107  isumz  11109  fsumf1o  11110  isumss  11111  fisumss  11112  isumss2  11113  fsum3cvg2  11114  fsum3cvg3  11116  fsum3ser  11117  fsumsplit  11127  fsumm1  11136  fsum1p  11138  fisumcom2  11158  fsumge1  11181  telfsumo  11186  telfsumo2  11187  fsumparts  11190  isumshft  11210  isum1p  11212  isumnn0nn  11213  isumrpcl  11214  cvgratnnlemnexp  11244  cvgratnnlemmn  11245  cvgratnnlemseq  11246  cvgratnnlemabsle  11247  cvgratnnlemfm  11249  cvgratnnlemrate  11250  cvgratnn  11251  cvgratz  11252  mertenslemi1  11255  mertenslem2  11256  mertensabs  11257  bezoutlemmain  11593  bezoutlemex  11596  bezoutlemzz  11597  bezoutlemmo  11601  bezoutlemle  11603  bezoutlemsup  11604  prmind2  11708  ennnfonelemk  11819  ennnfonelemex  11833  ennnfonelemnn0  11841  ctinfomlemom  11846  ctiunctlemudc  11856  icnpimaex  12286  lmcvg  12292  lmff  12324  cnmpt11  12358  cnmpt21  12366  comet  12574  dedekindeulemuub  12670  dedekindeulemloc  12672  dedekindeulemlu  12674  dedekindeulemeu  12675  suplociccreex  12677  suplociccex  12678  dedekindicclemuub  12679  dedekindicclemloc  12681  dedekindicclemlu  12683  dedekindicclemeu  12684  dedekindicc  12686  ivthinclemlopn  12689  ivthinclemlr  12690  ivthinclemuopn  12691  ivthinclemur  12692  ivthinclemdisj  12693  ivthinclemloc  12694  ivthinc  12696  ivthdec  12697  limcimolemlt  12708  limcimo  12709  cnplimclemr  12713  cnlimci  12717  cnmptlimc  12718  limccnpcntop  12719  limccoap  12722  dvcoapbr  12746  subctctexmid  13030  nnsf  13033  nninfalllemn  13036  nninfalllem1  13037  nninfsellemeqinf  13046  isomninnlem  13059  trilpolemlt1  13068  sin24declemlt  13076
  Copyright terms: Public domain W3C validator