Theorem rexcom4 3286

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 1959	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3072	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1851	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2163	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 275	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 304	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rexcomOLD  3289  rexcom4a  3290  2ex2rexrot  3296  reuind  3748  uni0b  4936  iuncom4  5004  dfiun2g  5032  dfiun2gOLD  5033  iunn0  5069  iunxiun  5099  iinexg  5340  inuni  5342  iunopab  5558  iunopabOLD  5559  xpiundi  5744  xpiundir  5745  cnvuni  5884  dmiun  5911  dmopab2rex  5915  elsnres  6019  rniun  6144  xpdifid  6164  imaco  6247  coiun  6252  abrexco  7238  imaiun  7239  fliftf  7307  imaeqsexv  7355  imaeqexov  7640  fiun  7924  f1iun  7925  oprabrexex2  7960  releldm2  8024  oarec  8558  omeu  8581  eroveu  8802  brttrcl2  9705  dfac5lem2  10115  genpass  11000  supaddc  12177  supadd  12178  supmul1  12179  supmullem2  12181  supmul  12182  pceu  16775  4sqlem12  16885  mreiincl  17536  psgneu  19367  ntreq0  22563  unisngl  23013  metrest  24015  metuel2  24056  nosupno  27186  nosupfv  27189  noinfno  27201  noinffv  27204  elold  27344  lrrecfr  27407  sleadd1  27452  addsuniflem  27464  addsasslem1  27466  addsasslem2  27467  mulsuniflem  27584  addsdilem1  27586  addsdilem2  27587  mulsasslem1  27598  mulsasslem2  27599  istrkg2ld  27691  fpwrelmapffslem  31935  omssubaddlem  33236  omssubadd  33237  bnj906  33879  satfdm  34298  dmopab3rexdif  34334  bj-elsngl  35787  bj-restn0  35909  ismblfin  36467  itg2addnclem3  36479  sdclem1  36549  eldmqs1cossres  37467  prter2  37689  lshpsmreu  37917  islpln5  38344  islvol5  38388  cdlemftr3  39374  mapdpglem3  40484  hdmapglem7a  40736  diophrex  41446  imaiun1  42335  coiun1  42336  grumnudlem  42977  upbdrech  43950