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

Theorem rexbidva 2432
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 1508 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2rexbida 2430 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    e. wcel 1480   E.wrex 2415
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-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-rex 2420
This theorem is referenced by:  2rexbiia  2449  2rexbidva  2456  rexeqbidva  2639  dfimafn  5463  funimass4  5465  fconstfvm  5631  fliftel  5687  fliftf  5693  f1oiso  5720  releldm2  6076  frecabcl  6289  qsinxp  6498  qliftel  6502  supisolem  6888  enumctlemm  6992  ismkvnex  7022  genpassl  7325  genpassu  7326  addcomprg  7379  mulcomprg  7381  1idprl  7391  1idpru  7392  archrecnq  7464  archrecpr  7465  caucvgprprlemexbt  7507  caucvgprprlemexb  7508  archsr  7583  map2psrprg  7606  suplocsrlempr  7608  axsuploc  7830  cnegexlem3  7932  cnegex2  7934  recexre  8333  rerecclap  8483  creur  8710  creui  8711  nndiv  8754  arch  8967  nnrecl  8968  expnlbnd  10409  fimaxq  10566  clim2  11045  clim2c  11046  clim0c  11048  climabs0  11069  climrecvg1n  11110  sumeq2  11121  mertensabs  11299  prodeq2  11319  nndivides  11489  alzdvds  11541  oddm1even  11561  oddnn02np1  11566  oddge22np1  11567  evennn02n  11568  evennn2n  11569  divalgb  11611  modremain  11615  iscnp3  12361  lmbrf  12373  cncnp  12388  lmss  12404  metrest  12664  metcnp  12670  metcnp2  12671  txmetcnp  12676  cdivcncfap  12745  ivthdec  12780
  Copyright terms: Public domain W3C validator