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

Theorem ralbi 2834
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 2748 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2758 . . 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 2711 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 1725   A.wral 2697
This theorem is referenced by:  uniiunlem  3423  iineq2  4102  reusv2lem5  4719  ralrnmpt  5869  f1mpt  5998  mpt22eqb  6170  ralrnmpt2  6175  rankonidlem  7743  acni2  7916  kmlem8  8026  kmlem13  8031  fimaxre3  9946  cau3lem  12146  rlim2  12278  rlim0  12290  rlim0lt  12291  catpropd  13923  funcres2b  14082  ulmss  20301  lgamgulmlem6  24806  colinearalg  25797  axpasch  25828  axcontlem2  25852  axcontlem4  25854  axcontlem7  25857  axcontlem8  25858  neibastop3  26328  ordelordALTVD  28833  pmapglbx  30405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator