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

Theorem ralbi 2680
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 2594 . 2  |-  F/ x A. x  e.  A  ( ph  <->  ps )
2 rsp 2604 . . 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 2558 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 1685   A.wral 2544
This theorem is referenced by:  uniiunlem  3261  iineq2  3923  reusv2lem5  4538  ralrnmpt  5631  f1mpt  5747  mpt22eqb  5915  ralrnmpt2  5920  rankonidlem  7496  acni2  7669  kmlem8  7779  kmlem13  7784  fimaxre3  9699  cau3lem  11834  rlim2  11966  rlim0  11978  rlim0lt  11979  catpropd  13608  funcres2b  13767  ulmss  19770  colinearalg  23948  axpasch  23979  axcontlem2  24003  axcontlem4  24005  axcontlem7  24008  axcontlem8  24009  svli2  24895  neibastop3  25722  ordelordALTVD  27923  pmapglbx  29237
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2549
  Copyright terms: Public domain W3C validator