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

Theorem ralbi 2957
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1686. (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 2804 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rspa 2790 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
31, 2ralbida 2856 1  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   A.wral 2773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-ral 2778
This theorem is referenced by:  uniiunlem  3546  iineq2  4311  reusv2lem5  4621  ralrnmpt  6037  f1mpt  6168  mpt22eqb  6410  ralrnmpt2  6416  rankonidlem  8289  acni2  8466  kmlem8  8576  kmlem13  8581  fimaxre3  10542  cau3lem  13385  rlim2  13527  rlim0  13539  rlim0lt  13540  catpropd  15566  funcres2b  15754  ulmss  23256  lgamgulmlem6  23863  colinearalg  24827  axpasch  24858  axcontlem2  24882  axcontlem4  24884  axcontlem7  24887  axcontlem8  24888  neibastop3  30844  ralbi12f  32152  iineq12f  32156  pmapglbx  33087  ordelordALTVD  36952
  Copyright terms: Public domain W3C validator