Theorem rexcom4 2827

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Assertion

Ref	Expression
rexcom4	|- ( E. x e. A E. y ph <-> E. y E. x e. A ph )

Distinct variable groups:   x, y   y, A

Allowed substitution hints:   ph( x, y)   A( x)

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		rexcom 2698	. 2 |- ( E. x e. A E. y e. _V ph <-> E. y e. _V E. x e. A ph )
2		rexv 2822	. . 3 |- ( E. y e. _V ph <-> E. y ph )
3	2	rexbii 2540	. 2 |- ( E. x e. A E. y e. _V ph <-> E. x e. A E. y ph )
4		rexv 2822	. 2 |- ( E. y e. _V E. x e. A ph <-> E. y E. x e. A ph )
5	1, 3, 4	3bitr3i 210	1 |- ( E. x e. A E. y ph <-> E. y E. x e. A ph )

Syntax hints:   <-> wb 105   E.wex 1541   E.wrex 2512   _Vcvv 2803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805

This theorem is referenced by:  rexcom4a  2828  reuind  3012  iuncom4  3982  dfiun2g  4007  iunn0m  4036  iunxiun  4057  iinexgm  4249  inuni  4250  iunopab  4382  xpiundi  4790  xpiundir  4791  cnvuni  4922  dmiun  4946  elres  5055  elsnres  5056  rniun  5154  imaco  5249  coiun  5253  fun11iun  5613  abrexco  5910  imaiun  5911  fliftf  5950  rexrnmpo  6147  oprabrexex2  6301  releldm2  6357  eroveu  6838  genpassl  7787  genpassu  7788  ltexprlemopl  7864  ltexprlemopu  7866  pceu  12931  4sqlem12  13038  ntreq0  14926  metrest  15300