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

Theorem ralcom4 3284
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.) (Proof shortened by Wolf Lammen, 31-Oct-2024.)
Assertion
Ref Expression
ralcom4 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralcom4
StepHypRef Expression
1 19.21v 1937 . . . 4 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21albii 1816 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
3 alcom 2157 . . 3 (∀𝑦𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 df-ral 3060 . . 3 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
52, 3, 43bitr4ri 304 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3060 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
76albii 1816 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
85, 7bitr4i 278 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  wcel 2106  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-11 2155
This theorem depends on definitions:  df-bi 207  df-ex 1777  df-ral 3060
This theorem is referenced by:  moelOLD  3403  ralxpxfr2d  3646  uniiunlem  4097  iunssf  5049  iunss  5050  disjor  5130  reliun  5829  idrefALT  6134  funimass4  6973  fnssintima  7382  ralrnmpo  7572  imaeqalov  7672  ralxp3f  8161  findcard3  9316  findcard3OLD  9317  ttrclss  9758  kmlem12  10200  fimaxre3  12212  vdwmc2  17013  ramtlecl  17034  iunocv  21717  1stccn  23487  itg2leub  25784  eqscut2  27866  addsuniflem  28049  mulsuniflem  28190  mptelee  28925  nmoubi  30801  nmopub  31937  nmfnleub  31954  disjorf  32599  funcnv5mpt  32685  untuni  35689  elintfv  35746  heibor1lem  37796  ineleq  38336  inecmo  38337  pmapglbx  39752  ismnuprim  44290  setrec1lem2  48919
  Copyright terms: Public domain W3C validator