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

Theorem ralbi 2679
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 2593 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2603 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 418 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2557 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 176    e. wcel 1684   A.wral 2543
This theorem is referenced by:  uniiunlem  3260  iineq2  3922  reusv2lem5  4539  ralrnmpt  5669  f1mpt  5785  mpt22eqb  5953  ralrnmpt2  5958  rankonidlem  7500  acni2  7673  kmlem8  7783  kmlem13  7788  fimaxre3  9703  cau3lem  11838  rlim2  11970  rlim0  11982  rlim0lt  11983  catpropd  13612  funcres2b  13771  ulmss  19774  colinearalg  24538  axpasch  24569  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  svli2  25484  neibastop3  26311  ordelordALTVD  28643  pmapglbx  29958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator