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

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

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