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

Theorem ralbidva 2339
Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1437 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2337 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102    e. wcel 1409   A.wral 2323
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-4 1416  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328
This theorem is referenced by:  raleqbidva  2536  poinxp  4437  funimass4  5252  funimass3  5311  funconstss  5313  cocan1  5455  cocan2  5456  isocnv2  5480  isores2  5481  isoini2  5486  ofrfval  5748  ofrfval2  5755  dfsmo2  5933  smores  5938  smores2  5940  ac6sfi  6383  supisolem  6412  ordiso2  6415  caucvgsrlemcau  6935  zextlt  8390  prime  8396  fzshftral  9072  clim  10033  clim2  10035  clim2c  10036  clim0c  10038  climabs0  10059  climrecvg1n  10098  sqrt2irr  10251
  Copyright terms: Public domain W3C validator