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

Theorem ralcom4 3222
Description: Commutation of restricted and unrestricted universal quantifiers. (Contributed by NM, 26-Mar-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
ralcom4 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem ralcom4
StepHypRef Expression
1 ralcom 3096 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥𝐴 𝜑)
2 ralv 3217 . . 3 (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑)
32ralbii 2979 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑥𝐴𝑦𝜑)
4 ralv 3217 . 2 (∀𝑦 ∈ V ∀𝑥𝐴 𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1480  wral 2911  Vcvv 3198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ral 2916  df-v 3200
This theorem is referenced by:  ralxpxfr2d  3325  uniiunlem  3689  iunss  4559  disjor  4632  trint  4766  reliun  5237  funimass4  6245  ralrnmpt2  6772  findcard3  8200  kmlem12  8980  fimaxre3  10967  vdwmc2  15677  ramtlecl  15698  iunocv  20019  1stccn  21260  itg2leub  23495  mptelee  25769  nmoubi  27611  nmopub  28751  nmfnleub  28768  moel  29307  disjorf  29376  funcnv5mpt  29454  untuni  31571  elintfv  31648  heibor1lem  33588  pmapglbx  34881  ss2iundf  37777  iunssf  39089  setrec1lem2  42206
  Copyright terms: Public domain W3C validator