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

Theorem ralbidva 2376
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 1466 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2374 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103    e. wcel 1438   A.wral 2359
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-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  raleqbidva  2576  poinxp  4507  funimass4  5355  funimass3  5415  funconstss  5417  cocan1  5566  cocan2  5567  isocnv2  5591  isores2  5592  isoini2  5598  ofrfval  5864  ofrfval2  5871  dfsmo2  6052  smores  6057  smores2  6059  ac6sfi  6612  supisolem  6701  ordiso2  6726  caucvgsrlemcau  7336  suprleubex  8413  dfinfre  8415  zextlt  8836  prime  8843  fzshftral  9518  fimaxq  10231  clim  10665  clim2  10667  clim2c  10668  clim0c  10670  climabs0  10692  climrecvg1n  10733  mertenslem2  10926  mertensabs  10927  dfgcd2  11277  sqrt2irr  11415  elcncf2  11585  mulc1cncf  11600
  Copyright terms: Public domain W3C validator