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

Theorem ralcom4 3429
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 3297 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥𝐴 𝜑)
2 ralv 3424 . . 3 (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑)
32ralbii 3179 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑥𝐴𝑦𝜑)
4 ralv 3424 . 2 (∀𝑦 ∈ V ∀𝑥𝐴 𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 292 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1635  wral 3107  Vcvv 3402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-v 3404
This theorem is referenced by:  ralxpxfr2d  3532  uniiunlem  3900  iunss  4764  disjor  4837  trint  4972  reliun  5452  idrefALT  5730  funimass4  6475  ralrnmpt2  7012  findcard3  8449  kmlem12  9275  fimaxre3  11262  vdwmc2  15907  ramtlecl  15928  iunocv  20243  1stccn  21488  itg2leub  23725  mptelee  25999  nmoubi  27965  nmopub  29105  nmfnleub  29122  moel  29661  disjorf  29727  funcnv5mpt  29806  untuni  31917  elintfv  31993  heibor1lem  33925  ineleq  34438  inecmo  34439  pmapglbx  35555  ss2iundf  38456  iunssf  39761  setrec1lem2  43008
  Copyright terms: Public domain W3C validator