Theorem rexcom4 2826

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	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		rexcom 2697	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑)
2		rexv 2821	. . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
3	2	rexbii 2539	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑)
4		rexv 2821	. 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
5	1, 3, 4	3bitr3i 210	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 105  ∃wex 1540  ∃wrex 2511  Vcvv 2802

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804

This theorem is referenced by:  rexcom4a  2827  reuind  3011  iuncom4  3977  dfiun2g  4002  iunn0m  4031  iunxiun  4052  iinexgm  4244  inuni  4245  iunopab  4376  xpiundi  4784  xpiundir  4785  cnvuni  4916  dmiun  4940  elres  5049  elsnres  5050  rniun  5147  imaco  5242  coiun  5246  fun11iun  5604  abrexco  5900  imaiun  5901  fliftf  5940  rexrnmpo  6137  oprabrexex2  6292  releldm2  6348  eroveu  6795  genpassl  7744  genpassu  7745  ltexprlemopl  7821  ltexprlemopu  7823  pceu  12870  4sqlem12  12977  ntreq0  14859  metrest  15233