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

Theorem ralbidva 2473
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 1528 . 2  |-  F/ x ph
2 ralbidva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
31, 2ralbida 2471 1  |-  ( ph  ->  ( A. x  e.  A  ps  <->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    e. wcel 2148   A.wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  raleqbidva  2686  poinxp  4692  funimass4  5562  fnmptfvd  5616  funimass3  5628  funconstss  5630  cocan1  5782  cocan2  5783  isocnv2  5807  isores2  5808  isoini2  5814  ofrfval  6085  ofrfval2  6093  dfsmo2  6282  smores  6287  smores2  6289  ac6sfi  6892  supisolem  7001  ordiso2  7028  ismkvnex  7147  nninfwlporlemd  7164  caucvgsrlemcau  7780  suplocsrlempr  7794  axsuploc  8017  suprleubex  8897  dfinfre  8899  zextlt  9331  prime  9338  infregelbex  9584  fzshftral  10091  fimaxq  10788  clim  11270  clim2  11272  clim2c  11273  clim0c  11275  climabs0  11296  climrecvg1n  11337  mertenslem2  11525  mertensabs  11526  dfgcd2  11995  sqrt2irr  12142  pc11  12310  pcz  12311  1arith  12345  infpn2  12437  grpidpropdg  12682  mndpropd  12730  grppropd  12780  ringpropd  13040  oppr1g  13074  tgss2  13243  neipsm  13318  ssidcn  13374  lmbrf  13379  cnnei  13396  cnrest2  13400  lmss  13410  lmres  13412  ismet2  13518  elmopn2  13613  metss  13658  metrest  13670  metcnp  13676  metcnp2  13677  metcn  13678  txmetcnp  13682  divcnap  13719  elcncf2  13725  mulc1cncf  13740  cncfmet  13743  cdivcncfap  13751  limcdifap  13795  limcmpted  13796  cnlimc  13805  2sqlem6  14120  iswomni0  14452
  Copyright terms: Public domain W3C validator