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

Theorem ralbi 2681
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 2595 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2605 . . 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 2559 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 1686   A.wral 2545
This theorem is referenced by:  uniiunlem  3262  iineq2  3924  reusv2lem5  4541  ralrnmpt  5671  f1mpt  5787  mpt22eqb  5955  ralrnmpt2  5960  rankonidlem  7502  acni2  7675  kmlem8  7785  kmlem13  7790  fimaxre3  9705  cau3lem  11840  rlim2  11972  rlim0  11984  rlim0lt  11985  catpropd  13614  funcres2b  13773  ulmss  19776  colinearalg  24540  axpasch  24571  axcontlem2  24595  axcontlem4  24597  axcontlem7  24600  axcontlem8  24601  svli2  25495  neibastop3  26322  ordelordALTVD  28716  pmapglbx  30031
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator