MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralbi Unicode version

Theorem ralbi 2785
Description: Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification. (Contributed by NM, 6-Oct-2003.)
Assertion
Ref Expression
ralbi  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps ) )

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 2699 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2709 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 419 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2663 1  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    e. wcel 1717   A.wral 2649
This theorem is referenced by:  uniiunlem  3374  iineq2  4052  reusv2lem5  4668  ralrnmpt  5817  f1mpt  5946  mpt22eqb  6118  ralrnmpt2  6123  rankonidlem  7687  acni2  7860  kmlem8  7970  kmlem13  7975  fimaxre3  9889  cau3lem  12085  rlim2  12217  rlim0  12229  rlim0lt  12230  catpropd  13862  funcres2b  14021  ulmss  20180  lgamgulmlem6  24597  colinearalg  25563  axpasch  25594  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  axcontlem8  25624  neibastop3  26082  ordelordALTVD  28320  pmapglbx  29883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2654
  Copyright terms: Public domain W3C validator