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

Step	Hyp	Ref	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 )
3	2	ralbii 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 )
5	1, 3, 4	3bitr3i 279	1 |- ( A. x e. A A. y ph <-> A. y A. x e. A ph )

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