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

Theorem ralcom4 3352
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 3224 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥𝐴 𝜑)
2 ralv 3347 . . 3 (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑)
32ralbii 3106 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑥𝐴𝑦𝜑)
4 ralv 3347 . 2 (∀𝑦 ∈ V ∀𝑥𝐴 𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1618  wral 3038  Vcvv 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-v 3330
This theorem is referenced by:  ralxpxfr2d  3454  uniiunlem  3821  iunss  4701  disjor  4774  trint  4908  reliun  5383  funimass4  6397  ralrnmpt2  6928  findcard3  8356  kmlem12  9146  fimaxre3  11133  vdwmc2  15856  ramtlecl  15877  iunocv  20198  1stccn  21439  itg2leub  23671  mptelee  25945  nmoubi  27907  nmopub  29047  nmfnleub  29064  moel  29603  disjorf  29670  funcnv5mpt  29749  untuni  31864  elintfv  31940  heibor1lem  33890  ineleq  34411  inecmo  34412  pmapglbx  35527  ss2iundf  38422  iunssf  39731  setrec1lem2  42914
  Copyright terms: Public domain W3C validator