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

Theorem ralbi 2641
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 2555 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 ra4 2565 . . 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 2521 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 2509
This theorem is referenced by:  uniiunlem  3181  iineq2  3820  reusv2lem5  4430  ralrnmpt  5521  f1mpt  5637  mpt22eqb  5805  ralrnmpt2  5810  rankonidlem  7384  acni2  7557  kmlem8  7667  kmlem13  7672  fimaxre3  9583  cau3lem  11715  rlim2  11847  rlim0  11859  rlim0lt  11860  catpropd  13456  funcres2b  13615  ulmss  19606  colinearalg  23712  axpasch  23743  axcontlem2  23767  axcontlem4  23769  axcontlem7  23772  axcontlem8  23773  svli2  24650  neibastop3  25477  ordelordALTVD  27333  pmapglbx  28647
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 2513
  Copyright terms: Public domain W3C validator