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

Theorem ralcom4 3232
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 1931 . . . . 5 (∀𝑦(𝑥𝐴𝜑) ↔ (𝑥𝐴 → ∀𝑦𝜑))
21bicomi 225 . . . 4 ((𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦(𝑥𝐴𝜑))
32albii 1811 . . 3 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑥𝑦(𝑥𝐴𝜑))
4 alcom 2153 . . 3 (∀𝑥𝑦(𝑥𝐴𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
53, 4bitri 276 . 2 (∀𝑥(𝑥𝐴 → ∀𝑦𝜑) ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
6 df-ral 3140 . 2 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝜑))
7 df-ral 3140 . . 3 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
87albii 1811 . 2 (∀𝑦𝑥𝐴 𝜑 ↔ ∀𝑦𝑥(𝑥𝐴𝜑))
95, 6, 83bitr4i 304 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1526  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-11 2151
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-ral 3140
This theorem is referenced by:  ralxpxfr2d  3636  uniiunlem  4058  iunss  4960  disjor  5037  reliun  5682  idrefALT  5966  funimass4  6723  ralrnmpo  7278  findcard3  8749  kmlem12  9575  fimaxre3  11575  vdwmc2  16303  ramtlecl  16324  iunocv  20753  1stccn  21999  itg2leub  24262  mptelee  26608  nmoubi  28476  nmopub  29612  nmfnleub  29629  moel  30179  disjorf  30257  funcnv5mpt  30341  untuni  32832  elintfv  32904  heibor1lem  34968  ineleq  35489  inecmo  35490  pmapglbx  36785  ss2iundf  39882  ismnuprim  40507  iunssf  41229  setrec1lem2  44719
  Copyright terms: Public domain W3C validator