Theorem rexcom4 2879

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	⊢ (∃x ∈ A ∃yφ ↔ ∃y∃x ∈ A φ)

Distinct variable groups:   x,y   y,A

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

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		rexcom 2773	. 2 ⊢ (∃x ∈ A ∃y ∈ V φ ↔ ∃y ∈ V ∃x ∈ A φ)
2		rexv 2874	. . 3 ⊢ (∃y ∈ V φ ↔ ∃yφ)
3	2	rexbii 2640	. 2 ⊢ (∃x ∈ A ∃y ∈ V φ ↔ ∃x ∈ A ∃yφ)
4		rexv 2874	. 2 ⊢ (∃y ∈ V ∃x ∈ A φ ↔ ∃y∃x ∈ A φ)
5	1, 3, 4	3bitr3i 266	1 ⊢ (∃x ∈ A ∃yφ ↔ ∃y∃x ∈ A φ)

Syntax hints:   ↔ wb 176  ∃wex 1541  ∃wrex 2616  Vcvv 2860

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-rex 2621  df-v 2862

This theorem is referenced by:  rexcom4a  2880  reuind  3040  uni0b  3917  iuncom4  3977  dfiun2g  4000  iunn0  4027  iunxiun  4049  elpw12  4146  imacok  4283  unipw1  4326  dfaddc2  4382  addcass  4416  ltfinex  4465  ncfinlowerlem1  4483  nnpweqlem1  4523  vfinspss  4552  vfinncsp  4555  setconslem6  4737  xpiundi  4818  xpiundir  4819  cnvuni  4896  elimapw1  4945  elimapw12  4946  elimapw13  4947  elsnres  4997  imaco  5087  coiun  5091  fun11iun  5306  abrexco  5464  imaiun  5465  isomin  5497  dfdm4  5508  dfrn5  5509  xpassen  6058  enpw1pw  6076