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

Theorem ralbiia 2491
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
Hypothesis
Ref Expression
ralbiia.1  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ralbiia  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )

Proof of Theorem ralbiia
StepHypRef Expression
1 ralbiia.1 . . 3  |-  ( x  e.  A  ->  ( ph 
<->  ps ) )
21pm5.74i 180 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2487 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  frind  4352  poinxp  4695  soinxp  4696  seinxp  4697  dffun8  5244  funcnv3  5278  fncnv  5282  fnres  5332  fvreseq  5619  isoini2  5819  smores  6292  resixp  6732  pw1dc1  6912  finomni  7137  caucvgre  10989  xpscf  12765  bj-charfundcALT  14531
  Copyright terms: Public domain W3C validator