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

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

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 2925 . 2 𝑥𝑥𝐴 (𝜑𝜓)
2 rspa 2914 . 2 ((∀𝑥𝐴 (𝜑𝜓) ∧ 𝑥𝐴) → (𝜑𝜓))
31, 2ralbida 2965 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-ral 2901
This theorem is referenced by:  uniiunlem  3653  iineq2  4474  reusv2lem5  4799  ralrnmpt  6276  f1mpt  6419  mpt22eqb  6667  ralrnmpt2  6673  rankonidlem  8574  acni2  8752  kmlem8  8862  kmlem13  8867  fimaxre3  10849  cau3lem  13942  rlim2  14075  rlim0  14087  rlim0lt  14088  catpropd  16192  funcres2b  16380  ulmss  23955  lgamgulmlem6  24560  colinearalg  25590  axpasch  25621  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  neibastop3  31527  ralbi12f  33139  iineq12f  33143  pmapglbx  34073  ordelordALTVD  38125
  Copyright terms: Public domain W3C validator