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

Theorem ralbi 3134
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1800. (Contributed by NM, 6-Oct-2003.) Reduce axiom usage. (Revised by Wolf Lammen, 17-Jun-2023.)
Assertion
Ref Expression
ralbi (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))

Proof of Theorem ralbi
StepHypRef Expression
1 biimp 216 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21ral2imi 3123 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
3 biimpr 221 . . 3 ((𝜑𝜓) → (𝜓𝜑))
43ral2imi 3123 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜑))
52, 4impbid 213 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wral 3105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791
This theorem depends on definitions:  df-bi 208  df-ral 3110
This theorem is referenced by:  uniiunlem  3982  iineq2  4844  reusv2lem5  5194  ralrnmpt  6725  f1mpt  6884  mpo2eqb  7139  ralrnmpo  7145  rankonidlem  9103  acni2  9318  kmlem8  9429  kmlem13  9434  fimaxre3  11435  cau3lem  14548  rlim2  14687  rlim0  14699  rlim0lt  14700  catpropd  16808  funcres2b  16996  ulmss  24668  lgamgulmlem6  25293  colinearalg  26379  axpasch  26410  axcontlem2  26434  axcontlem4  26436  axcontlem7  26439  axcontlem8  26440  neibastop3  33320  bj-0int  34011  ralbi12f  34989  iineq12f  34993  pmapglbx  36455  ordelordALTVD  40759
  Copyright terms: Public domain W3C validator