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

Theorem rexbidva 2377
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 1466 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2375 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    e. wcel 1438   E.wrex 2360
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-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-rex 2365
This theorem is referenced by:  2rexbiia  2394  2rexbidva  2401  rexeqbidva  2577  dfimafn  5337  funimass4  5339  fconstfvm  5497  fliftel  5554  fliftf  5560  f1oiso  5587  releldm2  5937  frecabcl  6146  qsinxp  6348  qliftel  6352  supisolem  6682  genpassl  7062  genpassu  7063  addcomprg  7116  mulcomprg  7118  1idprl  7128  1idpru  7129  archrecnq  7201  archrecpr  7202  caucvgprprlemexbt  7244  caucvgprprlemexb  7245  archsr  7306  cnegexlem3  7638  cnegex2  7640  recexre  8031  rerecclap  8171  creur  8391  creui  8392  nndiv  8434  arch  8640  nnrecl  8641  expnlbnd  10043  fimaxq  10200  clim2  10635  clim2c  10636  clim0c  10638  climabs0  10660  climrecvg1n  10701  sumeq2  10712  nndivides  10885  alzdvds  10937  oddm1even  10957  oddnn02np1  10962  oddge22np1  10963  evennn02n  10964  evennn2n  10965  divalgb  11007  modremain  11011
  Copyright terms: Public domain W3C validator