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

Theorem rexbidva 2340
Description: Formula-building rule for restricted existential quantifier (deduction rule). (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 1437 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2338 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102    e. wcel 1409   E.wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-rex 2329
This theorem is referenced by:  2rexbiia  2357  2rexbidva  2364  rexeqbidva  2537  dfimafn  5250  funimass4  5252  fconstfvm  5407  fliftel  5461  fliftf  5467  f1oiso  5493  releldm2  5839  qsinxp  6213  qliftel  6217  supisolem  6412  genpassl  6680  genpassu  6681  addcomprg  6734  mulcomprg  6736  1idprl  6746  1idpru  6747  archrecnq  6819  archrecpr  6820  caucvgprprlemexbt  6862  caucvgprprlemexb  6863  archsr  6924  cnegexlem3  7251  cnegex2  7253  recexre  7643  rerecclap  7781  creur  7987  creui  7988  nndiv  8030  arch  8236  nnrecl  8237  expnlbnd  9541  clim2  10035  clim2c  10036  clim0c  10038  climabs0  10059  climrecvg1n  10098  nndivides  10115  alzdvds  10166  oddm1even  10186  oddnn02np1  10192  oddge22np1  10193  evennn02n  10194  evennn2n  10195  divalgb  10237  modremain  10241
  Copyright terms: Public domain W3C validator