Theorem rexcom4 3285

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		exdistr 1958	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3071	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1850	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2162	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 274	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3071	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 303	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-11 2154

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexcomOLD  3288  rexcom4a  3289  2ex2rexrot  3295  reuind  3749  uni0b  4937  iuncom4  5005  dfiun2g  5033  dfiun2gOLD  5034  iunn0  5070  iunxiun  5100  iinexg  5341  inuni  5343  iunopab  5559  iunopabOLD  5560  xpiundi  5746  xpiundir  5747  cnvuni  5886  dmiun  5913  dmopab2rex  5917  elsnres  6021  rniun  6147  xpdifid  6167  imaco  6250  coiun  6255  abrexco  7242  imaiun  7243  fliftf  7311  imaeqsexv  7359  imaeqexov  7644  fiun  7928  f1iun  7929  oprabrexex2  7964  releldm2  8028  oarec  8561  omeu  8584  eroveu  8805  brttrcl2  9708  dfac5lem2  10118  genpass  11003  supaddc  12180  supadd  12181  supmul1  12182  supmullem2  12184  supmul  12185  pceu  16778  4sqlem12  16888  mreiincl  17539  psgneu  19373  ntreq0  22580  unisngl  23030  metrest  24032  metuel2  24073  nosupno  27203  nosupfv  27206  noinfno  27218  noinffv  27221  elold  27361  lrrecfr  27424  sleadd1  27469  addsuniflem  27481  addsasslem1  27483  addsasslem2  27484  mulsuniflem  27601  addsdilem1  27603  addsdilem2  27604  mulsasslem1  27615  mulsasslem2  27616  istrkg2ld  27708  fpwrelmapffslem  31952  omssubaddlem  33293  omssubadd  33294  bnj906  33936  satfdm  34355  dmopab3rexdif  34391  bj-elsngl  35844  bj-restn0  35966  ismblfin  36524  itg2addnclem3  36536  sdclem1  36606  eldmqs1cossres  37524  prter2  37746  lshpsmreu  37974  islpln5  38401  islvol5  38445  cdlemftr3  39431  mapdpglem3  40541  hdmapglem7a  40793  diophrex  41503  imaiun1  42392  coiun1  42393  grumnudlem  43034  upbdrech  44005