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

Theorem ralcom4 3201
 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.)
Assertion
Ref Expression
ralcom4 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralcom4
StepHypRef Expression
1 19.21v 1940 . . . . 5 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21bicomi 227 . . . 4 ((𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥𝐴𝜑))
32albii 1821 . . 3 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 alcom 2161 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
53, 4bitri 278 . 2 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3114 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
7 df-ral 3114 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
87albii 1821 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
95, 6, 83bitr4i 306 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2112  ∀wral 3109 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-11 2159 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-ral 3114 This theorem is referenced by:  ralxpxfr2d  3590  uniiunlem  4015  iunssf  4934  iunss  4935  disjor  5013  reliun  5657  idrefALT  5944  funimass4  6709  ralrnmpo  7272  findcard3  8749  kmlem12  9576  fimaxre3  11579  vdwmc2  16308  ramtlecl  16329  iunocv  20373  1stccn  22071  itg2leub  24341  mptelee  26692  nmoubi  28558  nmopub  29694  nmfnleub  29711  moel  30262  disjorf  30345  funcnv5mpt  30434  untuni  33043  elintfv  33115  heibor1lem  35240  ineleq  35761  inecmo  35762  pmapglbx  37058  ss2iundf  40347  ismnuprim  40989  setrec1lem2  45205
 Copyright terms: Public domain W3C validator