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

Theorem rspcdva 2768
Description: Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.)
Hypotheses
Ref Expression
rspcdva.1  |-  ( x  =  C  ->  ( ps 
<->  ch ) )
rspcdva.2  |-  ( ph  ->  A. x  e.  A  ps )
rspcdva.3  |-  ( ph  ->  C  e.  A )
Assertion
Ref Expression
rspcdva  |-  ( ph  ->  ch )
Distinct variable groups:    x, A    x, C    ch, x
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rspcdva
StepHypRef Expression
1 rspcdva.3 . 2  |-  ( ph  ->  C  e.  A )
2 rspcdva.2 . 2  |-  ( ph  ->  A. x  e.  A  ps )
3 rspcdva.1 . . 3  |-  ( x  =  C  ->  ( ps 
<->  ch ) )
43rspcv 2759 . 2  |-  ( C  e.  A  ->  ( A. x  e.  A  ps  ->  ch ) )
51, 2, 4sylc 62 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316    e. wcel 1465   A.wral 2393
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 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-v 2662
This theorem is referenced by:  frirrg  4242  wetriext  4461  tfisi  4471  omsinds  4505  grprinvlem  5933  grprinvd  5934  suppssov1  5947  caofref  5971  caofinvl  5972  oprssdmm  6037  tfrlem1  6173  tfrlem5  6179  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemaccex  6213  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemaccex  6226  tfrcllemres  6227  tfrcl  6229  rdgon  6251  frecabcl  6264  undifdcss  6779  ctssdclemn0  6963  ctssdc  6966  enomnilem  6978  fodju0  6987  fodjuomnilemres  6988  ismkvnex  6997  fodjumkvlemres  7001  exmidaclem  7032  prltlu  7263  cauappcvgprlemm  7421  caucvgprlemm  7444  caucvgprprlemml  7470  suplocexprlemmu  7494  suplocexprlemdisj  7496  suplocexprlemloc  7497  suplocexprlemub  7499  caucvgsrlemgt1  7571  caucvgsr  7578  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axcaucvglemcau  7674  axcaucvglemres  7675  axpre-suploclemres  7677  exbtwnzlemstep  9980  apbtwnz  10002  frecuzrdgsuc  10142  frecuzrdgg  10144  frecuzrdgsuctlem  10151  uzsinds  10170  iseqovex  10184  seq3val  10186  seqvalcd  10187  seq3-1  10188  seqf  10189  seq3p1  10190  seqovcd  10191  seqp1cd  10194  seq3clss  10195  seq3fveq2  10197  seq3fveq  10199  seq3feq  10200  seq3shft2  10201  monoord  10204  monoord2  10205  ser3mono  10206  seq3split  10207  seq3caopr3  10209  iseqf1olemkle  10212  iseqf1olemklt  10213  iseqf1olemjpcl  10223  iseqf1olemqpcl  10224  iseqf1olemfvp  10225  seq3f1olemqsumkj  10226  seq3f1olemqsum  10228  seq3f1oleml  10231  seq3f1o  10232  seq3id3  10235  seq3id  10236  seq3id2  10237  seq3homo  10238  seq3z  10239  ser3ge0  10245  zfz1isolemiso  10537  seq3shft  10565  cvg1nlemcau  10711  cvg1nlemres  10712  recvguniq  10722  resqrexlemgt0  10747  resqrexlemoverl  10748  resqrexlemglsq  10749  climi  11011  climcn1  11032  serf0  11076  fsum3cvg  11101  summodclem2  11106  summodc  11107  fsum3  11111  isumz  11113  fsumf1o  11114  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsum3cvg3  11120  fsum3ser  11121  fsumsplit  11131  fsumm1  11140  fsum1p  11142  fisumcom2  11162  fsumge1  11185  telfsumo  11190  telfsumo2  11191  fsumparts  11194  isumshft  11214  isum1p  11216  isumnn0nn  11217  isumrpcl  11218  cvgratnnlemnexp  11248  cvgratnnlemmn  11249  cvgratnnlemseq  11250  cvgratnnlemabsle  11251  cvgratnnlemfm  11253  cvgratnnlemrate  11254  cvgratnn  11255  cvgratz  11256  mertenslemi1  11259  mertenslem2  11260  mertensabs  11261  bezoutlemmain  11598  bezoutlemex  11601  bezoutlemzz  11602  bezoutlemmo  11606  bezoutlemle  11608  bezoutlemsup  11609  prmind2  11713  ennnfonelemk  11824  ennnfonelemex  11838  ennnfonelemnn0  11846  ctinfomlemom  11851  ctiunctlemudc  11861  icnpimaex  12291  lmcvg  12297  lmff  12329  cnmpt11  12363  cnmpt21  12371  comet  12579  dedekindeulemuub  12675  dedekindeulemloc  12677  dedekindeulemlu  12679  dedekindeulemeu  12680  suplociccreex  12682  suplociccex  12683  dedekindicclemuub  12684  dedekindicclemloc  12686  dedekindicclemlu  12688  dedekindicclemeu  12689  dedekindicc  12691  ivthinclemlopn  12694  ivthinclemlr  12695  ivthinclemuopn  12696  ivthinclemur  12697  ivthinclemdisj  12698  ivthinclemloc  12699  ivthinc  12701  ivthdec  12702  limcimolemlt  12713  limcimo  12714  cnplimclemr  12718  cnlimci  12722  cnmptlimc  12723  limccnpcntop  12724  limccoap  12727  dvcoapbr  12751  sin0pilem2  12774  pilem3  12775  subctctexmid  13092  nnsf  13095  nninfalllemn  13098  nninfalllem1  13099  nninfsellemeqinf  13108  isomninnlem  13121  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator