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

Theorem ralbi 3103
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1818. (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 215 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21ral2imi 3085 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
3 biimpr 220 . . 3 ((𝜑𝜓) → (𝜓𝜑))
43ral2imi 3085 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜑))
52, 4impbid 212 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ral 3062
This theorem is referenced by:  rexbiOLD  3105  uniiunlem  4087  iineq2  5012  reusv2lem5  5402  ralrnmptw  7114  ralrnmpt  7116  f1mpt  7281  mpo2eqb  7565  ralrnmpo  7572  naddcom  8720  naddrid  8721  naddass  8734  rankonidlem  9868  acni2  10086  kmlem8  10198  kmlem13  10203  fimaxre3  12214  cau3lem  15393  rlim2  15532  rlim0  15544  rlim0lt  15545  catpropd  17752  funcres2b  17942  ulmss  26440  lgamgulmlem6  27077  colinearalg  28925  axpasch  28956  axcontlem2  28980  axcontlem4  28982  axcontlem7  28985  axcontlem8  28986  neibastop3  36363  bj-0int  37102  ralbi12f  38167  iineq12f  38171  pmapglbx  39771  ordelordALTVD  44887
  Copyright terms: Public domain W3C validator