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

Theorem ralbi 3092
Description: Distribute a restricted universal quantifier over a biconditional. Restricted quantification version of albi 1812. (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 214 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21ral2imi 3074 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓))
3 biimpr 219 . . 3 ((𝜑𝜓) → (𝜓𝜑))
43ral2imi 3074 . 2 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜑))
52, 4impbid 211 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-ral 3051
This theorem is referenced by:  rexbiOLD  3094  uniiunlem  4080  iineq2  5017  reusv2lem5  5402  ralrnmptw  7103  ralrnmpt  7105  f1mpt  7271  mpo2eqb  7553  ralrnmpo  7560  naddcom  8703  naddrid  8704  naddass  8717  rankonidlem  9858  acni2  10076  kmlem8  10187  kmlem13  10192  fimaxre3  12198  cau3lem  15342  rlim2  15481  rlim0  15493  rlim0lt  15494  catpropd  17697  funcres2b  17891  ulmss  26383  lgamgulmlem6  27016  colinearalg  28798  axpasch  28829  axcontlem2  28853  axcontlem4  28855  axcontlem7  28858  axcontlem8  28859  neibastop3  35979  bj-0int  36713  ralbi12f  37766  iineq12f  37770  pmapglbx  39374  ordelordALTVD  44450
  Copyright terms: Public domain W3C validator