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

Theorem ralbi 2998
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 2848 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rspa 2834 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
31, 2ralbida 2900 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 184   A.wral 2817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-ral 2822
This theorem is referenced by:  uniiunlem  3593  iineq2  4349  reusv2lem5  4658  ralrnmpt  6041  f1mpt  6168  mpt22eqb  6406  ralrnmpt2  6412  rankonidlem  8258  acni2  8439  kmlem8  8549  kmlem13  8554  fimaxre3  10504  cau3lem  13166  rlim2  13298  rlim0  13310  rlim0lt  13311  catpropd  14981  funcres2b  15140  ulmss  22657  colinearalg  24045  axpasch  24076  axcontlem2  24100  axcontlem4  24102  axcontlem7  24105  axcontlem8  24106  lgamgulmlem6  28408  neibastop3  30114  ralbi12f  30503  iineq12f  30507  ordelordALTVD  33153  pmapglbx  34971
  Copyright terms: Public domain W3C validator