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

Theorem ralbi 3083
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1825. (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 218 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21ral2imi 3072 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
3 biimpr 223 . . 3 ((𝜑𝜓) → (𝜓𝜑))
43ral2imi 3072 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜑))
52, 4impbid 215 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wral 3054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816
This theorem depends on definitions:  df-bi 210  df-ral 3059
This theorem is referenced by:  rexbi  3156  uniiunlem  3985  iineq2  4911  reusv2lem5  5279  ralrnmptw  6882  ralrnmpt  6884  f1mpt  7042  mpo2eqb  7310  ralrnmpo  7316  rankonidlem  9342  acni2  9558  kmlem8  9669  kmlem13  9674  fimaxre3  11676  cau3lem  14816  rlim2  14955  rlim0  14967  rlim0lt  14968  catpropd  17095  funcres2b  17284  ulmss  25156  lgamgulmlem6  25783  colinearalg  26868  axpasch  26899  axcontlem2  26923  axcontlem4  26925  axcontlem7  26928  axcontlem8  26929  naddcom  33490  naddid1  33491  neibastop3  34206  bj-0int  34925  ralbi12f  35973  iineq12f  35977  pmapglbx  37438  ordelordALTVD  42065
  Copyright terms: Public domain W3C validator