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

Theorem ralcom4 3089
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  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)

Proof of Theorem ralcom4
StepHypRef Expression
1 ralcom 2979 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 3084 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2831 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 3084 . 2  |-  ( A. y  e.  _V  A. x  e.  A  ph  <->  A. y A. x  e.  A  ph )
51, 3, 43bitr3i 275 1  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1368   A.wral 2795   _Vcvv 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3072
This theorem is referenced by:  ralxpxfr2d  3183  uniiunlem  3540  iunss  4311  disjor  4376  trint  4500  reliun  5060  funimass4  5843  ralrnmpt2  6307  findcard3  7658  kmlem12  8433  fimaxre3  10382  vdwmc2  14144  ramtlecl  14165  iunocv  18217  1stccn  19185  itg2leub  21330  mptelee  23278  nmoubi  24309  nmopub  25449  nmfnleub  25466  moel  26004  disjorf  26059  funcnv5mpt  26124  untuni  27496  heibor1lem  28848  pmapglbx  33721
  Copyright terms: Public domain W3C validator