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