Theorem rexcom4 3292

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 1977	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3090	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1871	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2199	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 278	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 307	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-11 2194

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  rexcom4a  3295  2ex2rexrot  3300  reuind  3719  uni0b  4895  iuncom4  4961  dfiun2g  4990  iunn0  5027  iunxiun  5059  iinexg  5309  inuni  5311  iunopab  5535  xpiundi  5723  xpiundir  5724  cnvuni  5867  dmiun  5894  dmopab2rex  5898  elsnres  6011  rniun  6136  xpdifid  6157  xpdifcnvepel  6158  imaco  6242  coiun  6248  abrexco  7232  imaiun  7233  fliftf  7303  imaeqsexvOLD  7351  imaeqexov  7638  fiun  7928  f1iun  7929  oprabrexex2  7963  releldm2  8028  oarec  8535  omeu  8558  eroveu  8798  brttrcl2  9671  dfac5lem2  10096  genpass  10982  supaddc  12173  supadd  12174  supmul1  12175  supmullem2  12177  supmul  12178  pceu  16896  4sqlem12  17006  mreiincl  17638  psgneu  19567  ntreq0  23195  unisngl  23645  metrest  24642  metuel2  24683  nosupno  27825  nosupfv  27828  noinfno  27840  noinffv  27843  elold  28010  lrrecfr  28094  leadds1  28140  addsuniflem  28152  addsasslem1  28154  addsasslem2  28155  mulsuniflem  28300  addsdilem1  28302  addsdilem2  28303  mulsasslem1  28314  mulsasslem2  28315  elreno2  28646  renegscl  28649  readdscl  28650  remulscl  28653  istrkg2ld  28687  fpwrelmapffslem  32989  omssubaddlem  34606  omssubadd  34607  bnj906  35235  satfdm  35732  dmopab3rexdif  35768  rexxfr3dALT  36002  bj-elsngl  37465  bj-restn0  37592  ismblfin  38172  itg2addnclem3  38184  sdclem1  38254  eldmqs1cossres  39255  prter2  39517  lshpsmreu  39745  islpln5  40171  islvol5  40215  cdlemftr3  41201  mapdpglem3  42311  hdmapglem7a  42563  diophrex  43368  imaiun1  44239  coiun1  44240  grumnudlem  44859  upbdrech  45882  usgrgrtrirex  48570