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

Theorem ralcom4 2819
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 2713 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 2814 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2580 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 2814 . 2  |-  ( A. y  e.  _V  A. x  e.  A  ph  <->  A. y A. x  e.  A  ph )
51, 3, 43bitr3i 266 1  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530   A.wral 2556   _Vcvv 2801
This theorem is referenced by:  uniiunlem  3273  iunss  3959  disjor  4023  trint  4144  reliun  4822  funimass4  5589  ralrnmpt2  5974  findcard3  7116  kmlem12  7803  fimaxre3  9719  vdwmc2  13042  ramtlecl  13063  iunocv  16597  1stccn  17205  itg2leub  19105  nmoubi  21366  nmopub  22504  nmfnleub  22521  funcnv5mpt  23251  untuni  24070  mptelee  24595  heibor1lem  26636  ralxpxfr2d  26863  pmapglbx  30580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator