Theorem ralcom4 3224

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 3098	. 2 |- ( A. x e. A A. y e. _V ph <-> A. y e. _V A. x e. A ph )
2		ralv 3219	. . 3 |- ( A. y e. _V ph <-> A. y ph )
3	2	ralbii 2980	. 2 |- ( A. x e. A A. y e. _V ph <-> A. x e. A A. y ph )
4		ralv 3219	. 2 |- ( A. y e. _V A. x e. A ph <-> A. y A. x e. A ph )
5	1, 3, 4	3bitr3i 290	1 |- ( A. x e. A A. y ph <-> A. y A. x e. A ph )

Syntax hints:   <-> wb 196   A.wal 1481   A.wral 2912   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202

This theorem is referenced by:  ralxpxfr2d  3327  uniiunlem  3691  iunss  4561  disjor  4634  trint  4768  reliun  5239  funimass4  6247  ralrnmpt2  6775  findcard3  8203  kmlem12  8983  fimaxre3  10970  vdwmc2  15683  ramtlecl  15704  iunocv  20025  1stccn  21266  itg2leub  23501  mptelee  25775  nmoubi  27627  nmopub  28767  nmfnleub  28784  moel  29323  disjorf  29392  funcnv5mpt  29469  untuni  31586  elintfv  31662  heibor1lem  33608  ineleq  34119  inecmo  34120  pmapglbx  35055  ss2iundf  37951  iunssf  39263  setrec1lem2  42435