Theorem ralcom4 3125

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 3015	. 2 |- ( A. x e. A A. y e. _V ph <-> A. y e. _V A. x e. A ph )
2		ralv 3120	. . 3 |- ( A. y e. _V ph <-> A. y ph )
3	2	ralbii 2885	. 2 |- ( A. x e. A A. y e. _V ph <-> A. x e. A A. y ph )
4		ralv 3120	. 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 1396   A.wral 2804   _Vcvv 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108

This theorem is referenced by:  ralxpxfr2d  3221  uniiunlem  3574  iunss  4356  disjor  4424  trint  4547  reliun  5111  funimass4  5899  ralrnmpt2  6390  findcard3  7755  kmlem12  8532  fimaxre3  10487  vdwmc2  14581  ramtlecl  14602  iunocv  18885  1stccn  20130  itg2leub  22307  mptelee  24400  nmoubi  25885  nmopub  27025  nmfnleub  27042  moel  27580  disjorf  27650  funcnv5mpt  27738  untuni  29322  heibor1lem  30545  pmapglbx  35890