Theorem rexcom4 3249

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.) Reduce axiom dependencies. (Revised by BJ, 13-Jun-2019.)

Assertion

Ref	Expression
rexcom4	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

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

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		df-rex 3144	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		19.42v 1954	. . . . 5 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
3	2	bicomi 226	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
4	3	exbii 1848	. . 3 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5		excom 2169	. . . 4 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3144	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
7	6	bicomi 226	. . . . 5 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝐴 𝜑)
8	7	exbii 1848	. . . 4 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
9	5, 8	bitri 277	. . 3 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
10	4, 9	bitri 277	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑) ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
11	1, 10	bitri 277	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2161

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  2ex2rexrot  3250  rexcom4a  3251  rexcom  3355  reuind  3744  uni0b  4864  iuncom4  4927  dfiun2g  4955  dfiun2gOLD  4956  iunn0  4989  iunxiun  5019  iinexg  5244  inuni  5246  iunopab  5446  xpiundi  5622  xpiundir  5623  cnvuni  5757  dmiun  5782  dmopab2rex  5786  elsnres  5892  rniun  6006  xpdifid  6025  imaco  6104  coiun  6109  abrexco  7003  imaiun  7004  fliftf  7068  fiun  7644  f1iun  7645  oprabrexex2  7679  releldm2  7742  oarec  8188  omeu  8211  eroveu  8392  dfac5lem2  9550  genpass  10431  supaddc  11608  supadd  11609  supmul1  11610  supmullem2  11612  supmul  11613  pceu  16183  4sqlem12  16292  mreiincl  16867  psgneu  18634  ntreq0  21685  unisngl  22135  metrest  23134  metuel2  23175  istrkg2ld  26246  fpwrelmapffslem  30468  omssubaddlem  31557  omssubadd  31558  bnj906  32202  satfdm  32616  dmopab3rexdif  32652  nosupno  33203  nosupfv  33206  bj-elsngl  34283  bj-restn0  34384  ismblfin  34948  itg2addnclem3  34960  sdclem1  35033  eldmqs1cossres  35908  prter2  36032  lshpsmreu  36260  islpln5  36686  islvol5  36730  cdlemftr3  37716  mapdpglem3  38826  hdmapglem7a  39078  diophrex  39392  imaiun1  40016  coiun1  40017  grumnudlem  40641  upbdrech  41592