Theorem rexcom4 2680

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 2569	. 2 |- ( E. x e. A E. y e. _V ph <-> E. y e. _V E. x e. A ph )
2		rexv 2675	. . 3 |- ( E. y e. _V ph <-> E. y ph )
3	2	rexbii 2416	. 2 |- ( E. x e. A E. y e. _V ph <-> E. x e. A E. y ph )
4		rexv 2675	. 2 |- ( E. y e. _V E. x e. A ph <-> E. y E. x e. A ph )
5	1, 3, 4	3bitr3i 209	1 |- ( E. x e. A E. y ph <-> E. y E. x e. A ph )

Syntax hints:   <-> wb 104   E.wex 1451   E.wrex 2391   _Vcvv 2657

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-rex 2396  df-v 2659

This theorem is referenced by:  rexcom4a  2681  reuind  2858  iuncom4  3786  dfiun2g  3811  iunn0m  3839  iunxiun  3860  iinexgm  4039  inuni  4040  iunopab  4163  xpiundi  4557  xpiundir  4558  cnvuni  4685  dmiun  4708  elres  4813  elsnres  4814  rniun  4907  imaco  5002  coiun  5006  fun11iun  5344  abrexco  5614  imaiun  5615  fliftf  5654  rexrnmpo  5840  oprabrexex2  5982  releldm2  6037  eroveu  6474  genpassl  7280  genpassu  7281  ltexprlemopl  7357  ltexprlemopu  7359  ntreq0  12144  metrest  12495