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

Theorem rexbidva 2470
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
Assertion
Ref Expression
rexbidva  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rexbidva
StepHypRef Expression
1 nfv 1524 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2468 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    e. wcel 2144   E.wrex 2452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1443  ax-gen 1445  ax-ie1 1489  ax-ie2 1490  ax-4 1506  ax-17 1522  ax-ial 1530
This theorem depends on definitions:  df-bi 117  df-nf 1457  df-rex 2457
This theorem is referenced by:  2rexbiia  2489  2rexbidva  2496  rexeqbidva  2683  dfimafn  5553  funimass4  5555  fconstfvm  5723  fliftel  5781  fliftf  5787  f1oiso  5814  releldm2  6173  frecabcl  6387  qsinxp  6598  qliftel  6602  supisolem  6994  enumctlemm  7100  ismkvnex  7140  genpassl  7495  genpassu  7496  addcomprg  7549  mulcomprg  7551  1idprl  7561  1idpru  7562  archrecnq  7634  archrecpr  7635  caucvgprprlemexbt  7677  caucvgprprlemexb  7678  archsr  7753  map2psrprg  7776  suplocsrlempr  7778  axsuploc  8001  cnegexlem3  8105  cnegex2  8107  recexre  8506  rerecclap  8656  creur  8884  creui  8885  nndiv  8928  arch  9141  nnrecl  9142  expnlbnd  10609  fimaxq  10771  clim2  11255  clim2c  11256  clim0c  11258  climabs0  11279  climrecvg1n  11320  sumeq2  11331  mertensabs  11509  prodeq2  11529  zproddc  11551  nndivides  11768  alzdvds  11823  oddm1even  11843  oddnn02np1  11848  oddge22np1  11849  evennn02n  11850  evennn2n  11851  divalgb  11893  modremain  11897  modprmn0modprm0  12219  pythagtriplem2  12229  pythagtrip  12246  pceu  12258  mndpfo  12701  mndpropd  12703  grppropd  12751  iscnp3  13160  lmbrf  13172  cncnp  13187  lmss  13203  metrest  13463  metcnp  13469  metcnp2  13470  txmetcnp  13475  cdivcncfap  13544  ivthdec  13579  pw1nct  14199
  Copyright terms: Public domain W3C validator