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

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

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 3043 . 2 𝑥𝑥𝐴 (𝜑𝜓)
2 rspa 3032 . 2 ((∀𝑥𝐴 (𝜑𝜓) ∧ 𝑥𝐴) → (𝜑𝜓))
31, 2ralbida 3084 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wral 3014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-10 2132  ax-12 2160
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1818  df-nf 1823  df-ral 3019
This theorem is referenced by:  uniiunlem  3798  iineq2  4646  reusv2lem5  4978  ralrnmpt  6483  f1mpt  6633  mpt22eqb  6886  ralrnmpt2  6892  rankonidlem  8804  acni2  8982  kmlem8  9092  kmlem13  9097  fimaxre3  11083  cau3lem  14214  rlim2  14347  rlim0  14359  rlim0lt  14360  catpropd  16491  funcres2b  16679  ulmss  24271  lgamgulmlem6  24880  colinearalg  25910  axpasch  25941  axcontlem2  25965  axcontlem4  25967  axcontlem7  25970  axcontlem8  25971  neibastop3  32584  bj-0int  33282  ralbi12f  34201  iineq12f  34205  pmapglbx  35475  ordelordALTVD  39519
  Copyright terms: Public domain W3C validator