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

Theorem ralbi 2858
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 2771 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2781 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 429 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2734 1  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1756   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2725
This theorem is referenced by:  uniiunlem  3445  iineq2  4193  reusv2lem5  4502  ralrnmpt  5857  f1mpt  5979  mpt22eqb  6204  ralrnmpt2  6210  rankonidlem  8040  acni2  8221  kmlem8  8331  kmlem13  8336  fimaxre3  10284  cau3lem  12847  rlim2  12979  rlim0  12991  rlim0lt  12992  catpropd  14653  funcres2b  14812  ulmss  21867  colinearalg  23161  axpasch  23192  axcontlem2  23216  axcontlem4  23218  axcontlem7  23221  axcontlem8  23222  lgamgulmlem6  27025  neibastop3  28588  ralbi12f  28978  iineq12f  28982  ordelordALTVD  31608  pmapglbx  33418
  Copyright terms: Public domain W3C validator