Theorem ralcom4 2981

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 2871	. 2 |- ( A. x e. A A. y e. _V ph <-> A. y e. _V A. x e. A ph )
2		ralv 2976	. . 3 |- ( A. y e. _V ph <-> A. y ph )
3	2	ralbii 2729	. 2 |- ( A. x e. A A. y e. _V ph <-> A. x e. A A. y ph )
4		ralv 2976	. 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 1360   A.wral 2705   _Vcvv 2962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-v 2964

This theorem is referenced by:  ralxpxfr2d  3073  uniiunlem  3428  iunss  4199  disjor  4264  trint  4388  reliun  4947  funimass4  5730  ralrnmpt2  6194  findcard3  7543  kmlem12  8318  fimaxre3  10266  vdwmc2  14022  ramtlecl  14043  iunocv  17947  1stccn  18908  itg2leub  21053  mptelee  22963  nmoubi  23994  nmopub  25134  nmfnleub  25151  moel  25690  disjorf  25746  funcnv5mpt  25811  untuni  27206  heibor1lem  28549  pmapglbx  32983