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

Theorem ralcom4 2981
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 2871 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 2976 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2729 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 2976 . 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 1360   A.wral 2705   _Vcvv 2962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-v 2964
This theorem is referenced by:  ralxpxfr2d  3073  uniiunlem  3428  iunss  4199  disjor  4264  trint  4388  reliun  4947  funimass4  5730  ralrnmpt2  6194  findcard3  7543  kmlem12  8318  fimaxre3  10266  vdwmc2  14022  ramtlecl  14043  iunocv  17947  1stccn  18908  itg2leub  21053  mptelee  22963  nmoubi  23994  nmopub  25134  nmfnleub  25151  moel  25690  disjorf  25746  funcnv5mpt  25811  untuni  27206  heibor1lem  28549  pmapglbx  32983
  Copyright terms: Public domain W3C validator