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

Theorem spcegv 2748
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 2258 . 2  |-  F/_ x A
2 nfv 1493 . 2  |-  F/ x ps
3 spcgv.1 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3spcegf 2743 1  |-  ( A  e.  V  ->  ( ps  ->  E. x ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 104    = wceq 1316   E.wex 1453    e. wcel 1465
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-v 2662
This theorem is referenced by:  spcev  2754  eqeu  2827  absneu  3565  elunii  3711  axpweq  4065  euotd  4146  brcogw  4678  opeldmg  4714  breldmg  4715  dmsnopg  4980  dff3im  5533  elunirn  5635  unielxp  6040  op1steq  6045  tfr0dm  6187  tfrlemibxssdm  6192  tfrlemiex  6196  tfr1onlembxssdm  6208  tfr1onlemex  6212  tfrcllembxssdm  6221  tfrcllemex  6225  frecabcl  6264  ertr  6412  f1oen3g  6616  f1dom2g  6618  f1domg  6620  dom3d  6636  en1  6661  phpelm  6728  isinfinf  6759  ordiso  6889  djudom  6946  difinfsn  6953  ctm  6962  enumct  6968  djudoml  7043  djudomr  7044  recexnq  7166  ltexprlemrl  7386  ltexprlemru  7388  recexprlemm  7400  recexprlemloc  7407  recexprlem1ssl  7409  recexprlem1ssu  7410  axpre-suploclemres  7677  frecuzrdgtcl  10153  frecuzrdgfunlem  10160  fihasheqf1oi  10502  zfz1isolem1  10551  climeu  11033  fsum3  11124  eltg3  12153  uptx  12370  xblm  12513  bj-2inf  13063  subctctexmid  13123
  Copyright terms: Public domain W3C validator