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

Theorem ralbi 2641
 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

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 2555 . 2
2 ra4 2565 . . 3
32imp 420 . 2
41, 3ralbida 2521 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wcel 1621  wral 2509 This theorem is referenced by:  uniiunlem  3181  iineq2  3820  reusv2lem5  4430  ralrnmpt  5521  f1mpt  5637  mpt22eqb  5805  ralrnmpt2  5810  rankonidlem  7384  acni2  7557  kmlem8  7667  kmlem13  7672  fimaxre3  9583  cau3lem  11715  rlim2  11847  rlim0  11859  rlim0lt  11860  catpropd  13456  funcres2b  13615  ulmss  19606  colinearalg  23712  axpasch  23743  axcontlem2  23767  axcontlem4  23769  axcontlem7  23772  axcontlem8  23773  svli2  24650  neibastop3  25477  ordelordALTVD  27333  pmapglbx  28647 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2513
 Copyright terms: Public domain W3C validator