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

Theorem ralbi 2842
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 2756 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2766 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 419 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2719 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 177    e. wcel 1725   A.wral 2705
This theorem is referenced by:  uniiunlem  3431  iineq2  4110  reusv2lem5  4728  ralrnmpt  5878  f1mpt  6007  mpt22eqb  6179  ralrnmpt2  6184  rankonidlem  7754  acni2  7927  kmlem8  8037  kmlem13  8042  fimaxre3  9957  cau3lem  12158  rlim2  12290  rlim0  12302  rlim0lt  12303  catpropd  13935  funcres2b  14094  ulmss  20313  lgamgulmlem6  24818  colinearalg  25849  axpasch  25880  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  axcontlem8  25910  neibastop3  26391  ordelordALTVD  28979  pmapglbx  30566
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2710
  Copyright terms: Public domain W3C validator