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

Theorem ralcom4 3068
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 2953 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. y  e.  _V  A. x  e.  A  ph )
2 ralv 3063 . . 3  |-  ( A. y  e.  _V  ph  <->  A. y ph )
32ralbii 2821 . 2  |-  ( A. x  e.  A  A. y  e.  _V  ph  <->  A. x  e.  A  A. y ph )
4 ralv 3063 . 2  |-  ( A. y  e.  _V  A. x  e.  A  ph  <->  A. y A. x  e.  A  ph )
51, 3, 43bitr3i 279 1  |-  ( A. x  e.  A  A. y ph  <->  A. y A. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   A.wal 1444   A.wral 2739   _Vcvv 3047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-v 3049
This theorem is referenced by:  ralxpxfr2d  3166  uniiunlem  3519  iunss  4322  disjor  4390  trint  4515  reliun  4957  funimass4  5921  ralrnmpt2  6416  findcard3  7819  kmlem12  8596  fimaxre3  10560  vdwmc2  14941  ramtlecl  14963  iunocv  19256  1stccn  20490  itg2leub  22704  mptelee  24937  nmoubi  26425  nmopub  27573  nmfnleub  27590  moel  28131  disjorf  28201  funcnv5mpt  28284  untuni  30348  heibor1lem  32153  pmapglbx  33346  ss2iundf  36263
  Copyright terms: Public domain W3C validator