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

Theorem spcegv 2687
Description: Existential specialization, using implicit substitution. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
spcgv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
spcegv  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Distinct variable groups:    ps, x    x, A
Allowed substitution hints:    ph( x)    V( x)

Proof of Theorem spcegv
StepHypRef Expression
1 nfcv 2220 . 2  |-  F/_ x A
2 nfv 1462 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 2682 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1285   E.wex 1422    e. wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604
This theorem is referenced by:  spcev  2693  eqeu  2763  absneu  3472  elunii  3614  axpweq  3953  euotd  4017  brcogw  4532  opeldmg  4568  breldmg  4569  dmsnopg  4822  dff3im  5344  elunirn  5437  unielxp  5831  op1steq  5836  tfr0dm  5971  tfrlemibxssdm  5976  tfrlemiex  5980  tfr1onlembxssdm  5992  tfr1onlemex  5996  tfrcllembxssdm  6005  tfrcllemex  6009  frecabcl  6048  ertr  6187  f1oen3g  6301  f1dom2g  6303  f1domg  6305  dom3d  6321  en1  6346  phpelm  6401  ordiso  6506  recexnq  6642  ltexprlemrl  6862  ltexprlemru  6864  recexprlemm  6876  recexprlemloc  6883  recexprlem1ssl  6885  recexprlem1ssu  6886  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  sizeeqf1oi  9812  climeu  10273  bj-2inf  10891
  Copyright terms: Public domain W3C validator