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

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

Proof of Theorem ralbidva
StepHypRef Expression
1 nfv 1493 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2408 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    e. wcel 1465   A.wral 2393
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398
This theorem is referenced by:  raleqbidva  2617  poinxp  4578  funimass4  5440  funimass3  5504  funconstss  5506  cocan1  5656  cocan2  5657  isocnv2  5681  isores2  5682  isoini2  5688  ofrfval  5958  ofrfval2  5966  dfsmo2  6152  smores  6157  smores2  6159  ac6sfi  6760  supisolem  6863  ordiso2  6888  ismkvnex  6997  caucvgsrlemcau  7569  suplocsrlempr  7583  axsuploc  7805  suprleubex  8680  dfinfre  8682  zextlt  9111  prime  9118  fzshftral  9856  fimaxq  10541  clim  11018  clim2  11020  clim2c  11021  clim0c  11023  climabs0  11044  climrecvg1n  11085  mertenslem2  11273  mertensabs  11274  dfgcd2  11629  sqrt2irr  11767  tgss2  12175  neipsm  12250  ssidcn  12306  lmbrf  12311  cnnei  12328  cnrest2  12332  lmss  12342  lmres  12344  ismet2  12450  elmopn2  12545  metss  12590  metrest  12602  metcnp  12608  metcnp2  12609  metcn  12610  txmetcnp  12614  divcnap  12651  elcncf2  12657  mulc1cncf  12672  cncfmet  12675  cdivcncfap  12683  limcdifap  12727  limcmpted  12728  cnlimc  12737
  Copyright terms: Public domain W3C validator