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

Theorem ralcom4 3286
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 1939 . . . 4 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21albii 1819 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
3 alcom 2159 . . 3 (∀𝑦𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 df-ral 3062 . . 3 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
52, 3, 43bitr4ri 304 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3062 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
76albii 1819 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
85, 7bitr4i 278 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  wcel 2108  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  ax-5 1910  ax-11 2157
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-ral 3062
This theorem is referenced by:  moelOLD  3405  ralxpxfr2d  3646  uniiunlem  4087  iunssf  5044  iunss  5045  disjor  5125  reliun  5826  idrefALT  6131  funimass4  6973  fnssintima  7382  ralrnmpo  7572  imaeqalov  7672  ralxp3f  8162  findcard3  9318  findcard3OLD  9319  ttrclss  9760  kmlem12  10202  fimaxre3  12214  vdwmc2  17017  ramtlecl  17038  iunocv  21699  1stccn  23471  itg2leub  25769  eqscut2  27851  addsuniflem  28034  mulsuniflem  28175  mptelee  28910  nmoubi  30791  nmopub  31927  nmfnleub  31944  disjorf  32592  funcnv5mpt  32678  untuni  35709  elintfv  35765  heibor1lem  37816  ineleq  38355  inecmo  38356  pmapglbx  39771  ismnuprim  44313  setrec1lem2  49207
  Copyright terms: Public domain W3C validator