Theorem ralbi 3068

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1746. (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

Step	Hyp	Ref	Expression
1		nfra1 2941	. 2 |- F/ x A. x e. A ( ph <-> ps )
2		rspa 2930	. 2 |- ( ( A. x e. A ( ph <-> ps ) /\ x e. A ) -> ( ph <-> ps ) )
3	1, 2	ralbida 2982	1 |- ( A. x e. A ( ph <-> ps ) -> ( A. x e. A ph <-> A. x e. A ps ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-ral 2917

This theorem is referenced by:  uniiunlem  3691  iineq2  4538  reusv2lem5  4873  ralrnmpt  6368  f1mpt  6518  mpt22eqb  6769  ralrnmpt2  6775  rankonidlem  8691  acni2  8869  kmlem8  8979  kmlem13  8984  fimaxre3  10970  cau3lem  14094  rlim2  14227  rlim0  14239  rlim0lt  14240  catpropd  16369  funcres2b  16557  ulmss  24151  lgamgulmlem6  24760  colinearalg  25790  axpasch  25821  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  neibastop3  32357  bj-0int  33055  ralbi12f  33969  iineq12f  33973  pmapglbx  35055  ordelordALTVD  39103