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

Theorem ralcom4 3100
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 2989 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 3095 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2856 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 3095 . 2  |-  ( A. y  e.  _V  A. x  e.  A  ph  <->  A. y A. x  e.  A  ph )
51, 3, 43bitr3i 278 1  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   A.wal 1435   A.wral 2775   _Vcvv 3081
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-v 3083
This theorem is referenced by:  ralxpxfr2d  3196  uniiunlem  3549  iunss  4337  disjor  4405  trint  4530  reliun  4970  funimass4  5929  ralrnmpt2  6422  findcard3  7817  kmlem12  8592  fimaxre3  10554  vdwmc2  14917  ramtlecl  14939  iunocv  19231  1stccn  20465  itg2leub  22679  mptelee  24912  nmoubi  26399  nmopub  27547  nmfnleub  27564  moel  28105  disjorf  28179  funcnv5mpt  28262  untuni  30332  heibor1lem  32055  pmapglbx  33253  ss2iundf  36111
  Copyright terms: Public domain W3C validator