Theorem ralbi 2988

Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1639. (Contributed by NM, 6-Oct-2003.)

Assertion

Ref	Expression
ralbi

Proof of Theorem ralbi

Step	Hyp	Ref	Expression
1		nfra1 2838	. 2
2		rspa 2824	. 2
3	1, 2	ralbida 2890	1

Syntax hints:  ->wi 4  <->wb 184  A.wral 2807

This theorem is referenced by:  uniiunlem  3587  iineq2  4348  reusv2lem5  4657  ralrnmpt  6040  f1mpt  6169  mpt22eqb  6411  ralrnmpt2  6417  rankonidlem  8267  acni2  8448  kmlem8  8558  kmlem13  8563  fimaxre3  10517  cau3lem  13187  rlim2  13319  rlim0  13331  rlim0lt  13332  catpropd  15104  funcres2b  15266  ulmss  22792  colinearalg  24213  axpasch  24244  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  lgamgulmlem6  28576  neibastop3  30180  ralbi12f  30569  iineq12f  30573  ordelordALTVD  33667  pmapglbx  35493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-ral 2812