Theorem rexcom4 2878

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 2772	. 2 ⊢ (∃x ∈ A ∃y ∈ V φ ↔ ∃y ∈ V ∃x ∈ A φ)
2		rexv 2873	. . 3 ⊢ (∃y ∈ V φ ↔ ∃yφ)
3	2	rexbii 2639	. 2 ⊢ (∃x ∈ A ∃y ∈ V φ ↔ ∃x ∈ A ∃yφ)
4		rexv 2873	. 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 2615  Vcvv 2859

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 2478  df-rex 2620  df-v 2861

This theorem is referenced by:  rexcom4a  2879  reuind  3039  uni0b  3916  iuncom4  3976  dfiun2g  3999  iunn0  4026  iunxiun  4048  elpw12  4145  imacok  4282  unipw1  4325  dfaddc2  4381  addcass  4415  ltfinex  4464  ncfinlowerlem1  4482  nnpweqlem1  4522  vfinspss  4551  vfinncsp  4554  setconslem6  4736  xpiundi  4817  xpiundir  4818  cnvuni  4895  elimapw1  4944  elimapw12  4945  elimapw13  4946  elsnres  4996  imaco  5086  coiun  5090  fun11iun  5305  abrexco  5463  imaiun  5464  isomin  5496  dfdm4  5507  dfrn5  5508  xpassen  6057  enpw1pw  6075