Theorem ralcom4 3100

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 2989	. 2 |- ( A. x e. A A. y e. _V ph <-> A. y e. _V A. x e. A ph )
2		ralv 3095	. . 3 |- ( A. y e. _V ph <-> A. y ph )
3	2	ralbii 2856	. 2 |- ( A. x e. A A. y e. _V ph <-> A. x e. A A. y ph )
4		ralv 3095	. 2 |- ( A. y e. _V A. x e. A ph <-> A. y A. x e. A ph )
5	1, 3, 4	3bitr3i 278	1 |- ( A. x e. A A. y ph <-> A. y A. x e. A ph )

Syntax hints:   <-> wb 187   A.wal 1435   A.wral 2775   _Vcvv 3081

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-v 3083

This theorem is referenced by:  ralxpxfr2d  3196  uniiunlem  3549  iunss  4337  disjor  4405  trint  4530  reliun  4970  funimass4  5929  ralrnmpt2  6422  findcard3  7817  kmlem12  8592  fimaxre3  10554  vdwmc2  14917  ramtlecl  14939  iunocv  19231  1stccn  20465  itg2leub  22679  mptelee  24912  nmoubi  26399  nmopub  27547  nmfnleub  27564  moel  28105  disjorf  28179  funcnv5mpt  28262  untuni  30332  heibor1lem  32055  pmapglbx  33253  ss2iundf  36111