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

Theorem ralcom4 3274
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 1935 . . . 4 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21albii 1814 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
3 alcom 2149 . . 3 (∀𝑦𝑥(𝑥𝐴𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 df-ral 3052 . . 3 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
52, 3, 43bitr4ri 303 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3052 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
76albii 1814 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
85, 7bitr4i 277 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1532  wcel 2099  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-11 2147
This theorem depends on definitions:  df-bi 206  df-ex 1775  df-ral 3052
This theorem is referenced by:  moelOLD  3389  ralxpxfr2d  3630  uniiunlem  4080  iunssf  5044  iunss  5045  disjor  5125  reliun  5814  idrefALT  6115  funimass4  6959  fnssintima  7366  ralrnmpo  7557  imaeqalov  7657  ralxp3f  8143  findcard3  9312  findcard3OLD  9313  ttrclss  9756  kmlem12  10197  fimaxre3  12206  vdwmc2  16976  ramtlecl  16997  iunocv  21673  1stccn  23455  itg2leub  25752  eqscut2  27833  addsuniflem  28012  mulsuniflem  28147  mptelee  28826  nmoubi  30702  nmopub  31838  nmfnleub  31855  disjorf  32499  funcnv5mpt  32585  untuni  35544  elintfv  35601  heibor1lem  37523  ineleq  38065  inecmo  38066  pmapglbx  39481  ismnuprim  44005  setrec1lem2  48470
  Copyright terms: Public domain W3C validator