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

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
StepHypRef Expression
1 nfra1 2838 . 2
2 rspa 2824 . 2
31, 2ralbida 2890 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator