Theorem rexcom4 2803

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 2675	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑)
2		rexv 2798	. . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
3	2	rexbii 2517	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑)
4		rexv 2798	. 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
5	1, 3, 4	3bitr3i 210	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 105  ∃wex 1518  ∃wrex 2489  Vcvv 2779

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-rex 2494  df-v 2781

This theorem is referenced by:  rexcom4a  2804  reuind  2988  iuncom4  3951  dfiun2g  3976  iunn0m  4005  iunxiun  4026  iinexgm  4217  inuni  4218  iunopab  4349  xpiundi  4754  xpiundir  4755  cnvuni  4885  dmiun  4909  elres  5017  elsnres  5018  rniun  5115  imaco  5210  coiun  5214  fun11iun  5569  abrexco  5856  imaiun  5857  fliftf  5896  rexrnmpo  6091  oprabrexex2  6245  releldm2  6301  eroveu  6743  genpassl  7679  genpassu  7680  ltexprlemopl  7756  ltexprlemopu  7758  pceu  12784  4sqlem12  12891  ntreq0  14771  metrest  15145