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

Theorem ralcom4 2966
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 2860 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 2961 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2721 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 2961 . 2  |-  ( A. y  e.  _V  A. x  e.  A  ph  <->  A. y A. x  e.  A  ph )
51, 3, 43bitr3i 267 1  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549   A.wral 2697   _Vcvv 2948
This theorem is referenced by:  uniiunlem  3423  iunss  4124  disjor  4188  trint  4309  reliun  4987  funimass4  5769  ralrnmpt2  6176  findcard3  7342  kmlem12  8033  fimaxre3  9949  vdwmc2  13339  ramtlecl  13360  iunocv  16900  1stccn  17518  itg2leub  19618  nmoubi  22265  nmopub  23403  nmfnleub  23420  disjorf  24013  funcnv5mpt  24076  untuni  25150  mptelee  25826  heibor1lem  26509  ralxpxfr2d  26732  pmapglbx  30503
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950
  Copyright terms: Public domain W3C validator