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

Theorem ralcom4 3215
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 3095 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑦 ∈ V ∀𝑥𝐴 𝜑)
2 ralv 3210 . . 3 (∀𝑦 ∈ V 𝜑 ↔ ∀𝑦𝜑)
32ralbii 2979 . 2 (∀𝑥𝐴𝑦 ∈ V 𝜑 ↔ ∀𝑥𝐴𝑦𝜑)
4 ralv 3210 . 2 (∀𝑦 ∈ V ∀𝑥𝐴 𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
51, 3, 43bitr3i 290 1 (∀𝑥𝐴𝑦𝜑 ↔ ∀𝑦𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1478  wral 2912  Vcvv 3191
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-v 3193
This theorem is referenced by:  ralxpxfr2d  3316  uniiunlem  3674  iunss  4532  disjor  4602  trint  4733  reliun  5205  funimass4  6205  ralrnmpt2  6729  findcard3  8148  kmlem12  8928  fimaxre3  10915  vdwmc2  15602  ramtlecl  15623  iunocv  19939  1stccn  21171  itg2leub  23402  mptelee  25670  nmoubi  27467  nmopub  28607  nmfnleub  28624  moel  29163  disjorf  29228  funcnv5mpt  29303  untuni  31286  heibor1lem  33226  pmapglbx  34521  ss2iundf  37418  iunssf  38734  setrec1lem2  41702
  Copyright terms: Public domain W3C validator