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

Theorem ralcom4 3376
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 3246 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥𝐴 𝜑)
2 ralv 3371 . . 3 (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑)
32ralbii 3129 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑥𝐴𝑦𝜑)
4 ralv 3371 . 2 (∀𝑦 ∈ V ∀𝑥𝐴 𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1629  wral 3061  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-v 3353
This theorem is referenced by:  ralxpxfr2d  3477  uniiunlem  3841  iunss  4695  disjor  4768  trint  4901  reliun  5378  funimass4  6389  ralrnmpt2  6922  findcard3  8359  kmlem12  9185  fimaxre3  11172  vdwmc2  15890  ramtlecl  15911  iunocv  20242  1stccn  21487  itg2leub  23721  mptelee  25996  nmoubi  27967  nmopub  29107  nmfnleub  29124  moel  29663  disjorf  29730  funcnv5mpt  29809  untuni  31924  elintfv  32000  heibor1lem  33940  ineleq  34461  inecmo  34462  pmapglbx  35577  ss2iundf  38477  iunssf  39784  setrec1lem2  42963
  Copyright terms: Public domain W3C validator