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

Theorem ralcom4 3177
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 1899 . . . . 5 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21bicomi 216 . . . 4 ((𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥𝐴𝜑))
32albii 1783 . . 3 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 alcom 2096 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
53, 4bitri 267 . 2 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3088 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
7 df-ral 3088 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
87albii 1783 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
95, 6, 83bitr4i 295 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1506  wcel 2051  wral 3083
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-11 2094
This theorem depends on definitions:  df-bi 199  df-ex 1744  df-ral 3088
This theorem is referenced by:  ralxpxfr2d  3549  uniiunlem  3946  iunss  4832  disjor  4908  trintOLD  5044  reliun  5536  idrefALT  5811  funimass4  6558  ralrnmpo  7104  findcard3  8555  kmlem12  9380  fimaxre3  11387  vdwmc2  16170  ramtlecl  16191  iunocv  20543  1stccn  21791  itg2leub  24054  mptelee  26400  nmoubi  28342  nmopub  29482  nmfnleub  29499  moel  30050  disjorf  30113  funcnv5mpt  30193  untuni  32488  elintfv  32560  heibor1lem  34562  ineleq  35087  inecmo  35088  pmapglbx  36383  ss2iundf  39401  ismnuprim  40039  iunssf  40805  setrec1lem2  44188
  Copyright terms: Public domain W3C validator