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

Theorem ralcom4 3114
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 3004 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 3109 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2874 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 3109 . 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 1381   A.wral 2793   _Vcvv 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097
This theorem is referenced by:  ralxpxfr2d  3210  uniiunlem  3573  iunss  4356  disjor  4421  trint  4545  reliun  5113  funimass4  5909  ralrnmpt2  6402  findcard3  7765  kmlem12  8544  fimaxre3  10498  vdwmc2  14374  ramtlecl  14395  iunocv  18585  1stccn  19837  itg2leub  22014  mptelee  24070  nmoubi  25559  nmopub  26699  nmfnleub  26716  moel  27254  disjorf  27312  funcnv5mpt  27383  untuni  28954  heibor1lem  30280  pmapglbx  35233
  Copyright terms: Public domain W3C validator