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

Theorem ralbi 2849
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 2763 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2773 . . 3  |-  ( A. x  e.  A  ( ph 
<->  ps )  ->  (
x  e.  A  -> 
( ph  <->  ps ) ) )
32imp 420 . 2  |-  ( ( A. x  e.  A  ( ph  <->  ps )  /\  x  e.  A )  ->  ( ph 
<->  ps ) )
41, 3ralbida 2726 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 178    e. wcel 1728   A.wral 2712
This theorem is referenced by:  uniiunlem  3420  iineq2  4139  reusv2lem5  4763  ralrnmpt  5914  f1mpt  6043  mpt22eqb  6215  ralrnmpt2  6220  rankonidlem  7790  acni2  7965  kmlem8  8075  kmlem13  8080  fimaxre3  9995  cau3lem  12196  rlim2  12328  rlim0  12340  rlim0lt  12341  catpropd  13973  funcres2b  14132  ulmss  20351  lgamgulmlem6  24853  colinearalg  25884  axpasch  25915  axcontlem2  25939  axcontlem4  25941  axcontlem7  25944  axcontlem8  25945  neibastop3  26433  ralbi12f  26788  iineq12f  26792  ordelordALTVD  29153  pmapglbx  30740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-11 1764
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2717
  Copyright terms: Public domain W3C validator