Theorem rexcom4 3288

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2157

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  rexcomOLD  3291  rexcom4a  3292  2ex2rexrot  3298  reuind  3759  uni0b  4933  iuncom4  5000  dfiun2g  5030  dfiun2gOLD  5031  iunn0  5067  iunxiun  5097  iinexg  5348  inuni  5350  iunopab  5564  iunopabOLD  5565  xpiundi  5756  xpiundir  5757  cnvuni  5897  dmiun  5924  dmopab2rex  5928  elsnres  6039  rniun  6167  xpdifid  6188  imaco  6271  coiun  6276  abrexco  7264  imaiun  7265  fliftf  7335  imaeqsexvOLD  7383  imaeqexov  7671  fiun  7967  f1iun  7968  oprabrexex2  8003  releldm2  8068  oarec  8600  omeu  8623  eroveu  8852  brttrcl2  9754  dfac5lem2  10164  genpass  11049  supaddc  12235  supadd  12236  supmul1  12237  supmullem2  12239  supmul  12240  pceu  16884  4sqlem12  16994  mreiincl  17639  psgneu  19524  ntreq0  23085  unisngl  23535  metrest  24537  metuel2  24578  nosupno  27748  nosupfv  27751  noinfno  27763  noinffv  27766  elold  27908  lrrecfr  27976  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  mulsuniflem  28175  addsdilem1  28177  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  renegscl  28430  readdscl  28431  remulscl  28434  istrkg2ld  28468  fpwrelmapffslem  32743  omssubaddlem  34301  omssubadd  34302  bnj906  34944  satfdm  35374  dmopab3rexdif  35410  rexxfr3dALT  35644  bj-elsngl  36969  bj-restn0  37091  ismblfin  37668  itg2addnclem3  37680  sdclem1  37750  eldmqs1cossres  38660  prter2  38882  lshpsmreu  39110  islpln5  39537  islvol5  39581  cdlemftr3  40567  mapdpglem3  41677  hdmapglem7a  41929  diophrex  42786  imaiun1  43664  coiun1  43665  grumnudlem  44304  upbdrech  45317  usgrgrtrirex  47917