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

Theorem ralbi 3097
 Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1786. (Contributed by NM, 6-Oct-2003.)
Assertion
Ref Expression
ralbi (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 2970 . 2 𝑥𝑥𝐴 (𝜑𝜓)
2 rspa 2959 . 2 ((∀𝑥𝐴 (𝜑𝜓) ∧ 𝑥𝐴) → (𝜑𝜓))
31, 2ralbida 3011 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-ral 2946 This theorem is referenced by:  uniiunlem  3724  iineq2  4570  reusv2lem5  4903  ralrnmpt  6408  f1mpt  6558  mpt22eqb  6811  ralrnmpt2  6817  rankonidlem  8729  acni2  8907  kmlem8  9017  kmlem13  9022  fimaxre3  11008  cau3lem  14138  rlim2  14271  rlim0  14283  rlim0lt  14284  catpropd  16416  funcres2b  16604  ulmss  24196  lgamgulmlem6  24805  colinearalg  25835  axpasch  25866  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  neibastop3  32482  bj-0int  33180  ralbi12f  34099  iineq12f  34103  pmapglbx  35373  ordelordALTVD  39417
 Copyright terms: Public domain W3C validator