Theorem ralcom4 3089

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 2979	. 2 |- ( A. x e. A A. y e. _V ph <-> A. y e. _V A. x e. A ph )
2		ralv 3084	. . 3 |- ( A. y e. _V ph <-> A. y ph )
3	2	ralbii 2831	. 2 |- ( A. x e. A A. y e. _V ph <-> A. x e. A A. y ph )
4		ralv 3084	. 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 1368   A.wral 2795   _Vcvv 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-v 3072

This theorem is referenced by:  ralxpxfr2d  3183  uniiunlem  3540  iunss  4311  disjor  4376  trint  4500  reliun  5060  funimass4  5843  ralrnmpt2  6307  findcard3  7658  kmlem12  8433  fimaxre3  10382  vdwmc2  14144  ramtlecl  14165  iunocv  18217  1stccn  19185  itg2leub  21330  mptelee  23278  nmoubi  24309  nmopub  25449  nmfnleub  25466  moel  26004  disjorf  26059  funcnv5mpt  26124  untuni  27496  heibor1lem  28848  pmapglbx  33721