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

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

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 2936 . 2 𝑥𝑥𝐴 (𝜑𝜓)
2 rspa 2925 . 2 ((∀𝑥𝐴 (𝜑𝜓) ∧ 𝑥𝐴) → (𝜑𝜓))
31, 2ralbida 2976 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707  df-ral 2912
This theorem is referenced by:  uniiunlem  3669  iineq2  4504  reusv2lem5  4833  ralrnmpt  6324  f1mpt  6472  mpt22eqb  6722  ralrnmpt2  6728  rankonidlem  8635  acni2  8813  kmlem8  8923  kmlem13  8928  fimaxre3  10914  cau3lem  14028  rlim2  14161  rlim0  14173  rlim0lt  14174  catpropd  16290  funcres2b  16478  ulmss  24055  lgamgulmlem6  24660  colinearalg  25690  axpasch  25721  axcontlem2  25745  axcontlem4  25747  axcontlem7  25750  axcontlem8  25751  neibastop3  31996  ralbi12f  33598  iineq12f  33602  pmapglbx  34532  ordelordALTVD  38583
  Copyright terms: Public domain W3C validator