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

Theorem ralcom4 3125
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 3015 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 3120 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2885 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 3120 . 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 1396   A.wral 2804   _Vcvv 3106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108
This theorem is referenced by:  ralxpxfr2d  3221  uniiunlem  3574  iunss  4356  disjor  4424  trint  4547  reliun  5111  funimass4  5899  ralrnmpt2  6390  findcard3  7755  kmlem12  8532  fimaxre3  10487  vdwmc2  14581  ramtlecl  14602  iunocv  18885  1stccn  20130  itg2leub  22307  mptelee  24400  nmoubi  25885  nmopub  27025  nmfnleub  27042  moel  27580  disjorf  27650  funcnv5mpt  27738  untuni  29322  heibor1lem  30545  pmapglbx  35890
  Copyright terms: Public domain W3C validator