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

Theorem ralbi 2713
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 2627 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2637 . . 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 2591 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 1701   A.wral 2577
This theorem is referenced by:  uniiunlem  3294  iineq2  3959  reusv2lem5  4576  ralrnmpt  5707  f1mpt  5827  mpt22eqb  5995  ralrnmpt2  6000  rankonidlem  7545  acni2  7718  kmlem8  7828  kmlem13  7833  fimaxre3  9748  cau3lem  11885  rlim2  12017  rlim0  12029  rlim0lt  12030  catpropd  13661  funcres2b  13820  ulmss  19827  colinearalg  24924  axpasch  24955  axcontlem2  24979  axcontlem4  24981  axcontlem7  24984  axcontlem8  24985  neibastop3  25460  ordelordALTVD  28154  pmapglbx  29776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-nf 1536  df-ral 2582
  Copyright terms: Public domain W3C validator