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

Theorem ralbi 2654
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 2568 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 ra4 2578 . . 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 2532 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 2518
This theorem is referenced by:  uniiunlem  3235  iineq2  3896  reusv2lem5  4511  ralrnmpt  5603  f1mpt  5719  mpt22eqb  5887  ralrnmpt2  5892  rankonidlem  7468  acni2  7641  kmlem8  7751  kmlem13  7756  fimaxre3  9671  cau3lem  11804  rlim2  11936  rlim0  11948  rlim0lt  11949  catpropd  13575  funcres2b  13734  ulmss  19737  colinearalg  23914  axpasch  23945  axcontlem2  23969  axcontlem4  23971  axcontlem7  23974  axcontlem8  23975  svli2  24852  neibastop3  25679  ordelordALTVD  27776  pmapglbx  29208
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 2523
  Copyright terms: Public domain W3C validator