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

Theorem ralbi 2650
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 2564 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 ra4 2574 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 420 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2528 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 6    <-> wb 178    e. wcel 1621   A.wral 2516
This theorem is referenced by:  uniiunlem  3202  iineq2  3863  reusv2lem5  4476  ralrnmpt  5568  f1mpt  5684  mpt22eqb  5852  ralrnmpt2  5857  rankonidlem  7433  acni2  7606  kmlem8  7716  kmlem13  7721  fimaxre3  9636  cau3lem  11768  rlim2  11900  rlim0  11912  rlim0lt  11913  catpropd  13539  funcres2b  13698  ulmss  19701  colinearalg  23878  axpasch  23909  axcontlem2  23933  axcontlem4  23935  axcontlem7  23938  axcontlem8  23939  svli2  24816  neibastop3  25643  ordelordALTVD  27656  pmapglbx  29088
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2520
  Copyright terms: Public domain W3C validator