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

Theorem ralbidva 2434
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 1509 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2432 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 1481   A.wral 2417
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422
This theorem is referenced by:  raleqbidva  2643  poinxp  4615  funimass4  5479  funimass3  5543  funconstss  5545  cocan1  5695  cocan2  5696  isocnv2  5720  isores2  5721  isoini2  5727  ofrfval  5997  ofrfval2  6005  dfsmo2  6191  smores  6196  smores2  6198  ac6sfi  6799  supisolem  6902  ordiso2  6927  ismkvnex  7036  caucvgsrlemcau  7624  suplocsrlempr  7638  axsuploc  7860  suprleubex  8735  dfinfre  8737  zextlt  9166  prime  9173  fzshftral  9918  fimaxq  10604  clim  11081  clim2  11083  clim2c  11084  clim0c  11086  climabs0  11107  climrecvg1n  11148  mertenslem2  11336  mertensabs  11337  dfgcd2  11736  sqrt2irr  11874  tgss2  12285  neipsm  12360  ssidcn  12416  lmbrf  12421  cnnei  12438  cnrest2  12442  lmss  12452  lmres  12454  ismet2  12560  elmopn2  12655  metss  12700  metrest  12712  metcnp  12718  metcnp2  12719  metcn  12720  txmetcnp  12724  divcnap  12761  elcncf2  12767  mulc1cncf  12782  cncfmet  12785  cdivcncfap  12793  limcdifap  12837  limcmpted  12838  cnlimc  12847
  Copyright terms: Public domain W3C validator