Theorem rexcom4 3264

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

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 1912  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexcom4a  3267  2ex2rexrot  3272  reuind  3712  uni0b  4890  iuncom4  4956  dfiun2g  4986  iunn0  5023  iunxiun  5053  iinexg  5294  inuni  5296  iunopab  5508  xpiundi  5696  xpiundir  5697  cnvuni  5836  dmiun  5863  dmopab2rex  5867  elsnres  5981  rniun  6106  xpdifid  6127  imaco  6210  coiun  6216  abrexco  7192  imaiun  7193  fliftf  7263  imaeqsexvOLD  7311  imaeqexov  7598  fiun  7889  f1iun  7890  oprabrexex2  7924  releldm2  7989  oarec  8491  omeu  8514  eroveu  8753  brttrcl2  9627  dfac5lem2  10038  genpass  10924  supaddc  12113  supadd  12114  supmul1  12115  supmullem2  12117  supmul  12118  pceu  16778  4sqlem12  16888  mreiincl  17519  psgneu  19439  ntreq0  23025  unisngl  23475  metrest  24472  metuel2  24513  nosupno  27675  nosupfv  27678  noinfno  27690  noinffv  27693  elold  27851  lrrecfr  27925  sleadd1  27971  addsuniflem  27983  addsasslem1  27985  addsasslem2  27986  mulsuniflem  28131  addsdilem1  28133  addsdilem2  28134  mulsasslem1  28145  mulsasslem2  28146  elreno2  28474  renegscl  28477  readdscl  28478  remulscl  28481  istrkg2ld  28515  fpwrelmapffslem  32792  omssubaddlem  34437  omssubadd  34438  bnj906  35067  satfdm  35544  dmopab3rexdif  35580  rexxfr3dALT  35814  bj-elsngl  37144  bj-restn0  37266  ismblfin  37833  itg2addnclem3  37845  sdclem1  37915  eldmqs1cossres  38916  prter2  39178  lshpsmreu  39406  islpln5  39832  islvol5  39876  cdlemftr3  40862  mapdpglem3  41972  hdmapglem7a  42224  diophrex  43053  imaiun1  43928  coiun1  43929  grumnudlem  44562  upbdrech  45589  usgrgrtrirex  48232