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

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

Proof of Theorem ralbi
StepHypRef Expression
1 nfra1 3088 . 2 𝑥𝑥𝐴 (𝜑𝜓)
2 rspa 3077 . 2 ((∀𝑥𝐴 (𝜑𝜓) ∧ 𝑥𝐴) → (𝜑𝜓))
31, 2ralbida 3129 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-10 2183  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ex 1875  df-nf 1879  df-ral 3060
This theorem is referenced by:  uniiunlem  3852  iineq2  4694  reusv2lem5  5037  ralrnmpt  6558  f1mpt  6710  mpt22eqb  6967  ralrnmpt2  6973  rankonidlem  8906  acni2  9120  kmlem8  9232  kmlem13  9237  fimaxre3  11224  cau3lem  14381  rlim2  14514  rlim0  14526  rlim0lt  14527  catpropd  16636  funcres2b  16824  ulmss  24442  lgamgulmlem6  25051  colinearalg  26081  axpasch  26112  axcontlem2  26136  axcontlem4  26138  axcontlem7  26141  axcontlem8  26142  neibastop3  32732  bj-0int  33415  ralbi12f  34322  iineq12f  34326  pmapglbx  35657  ordelordALTVD  39687
  Copyright terms: Public domain W3C validator