Theorem rexcom4 3265

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

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

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 3063

This theorem is referenced by:  rexcom4a  3268  2ex2rexrot  3273  reuind  3713  uni0b  4891  iuncom4  4957  dfiun2g  4987  iunn0  5024  iunxiun  5054  iinexg  5295  inuni  5297  iunopab  5515  xpiundi  5703  xpiundir  5704  cnvuni  5843  dmiun  5870  dmopab2rex  5874  elsnres  5988  rniun  6113  xpdifid  6134  imaco  6217  coiun  6223  abrexco  7200  imaiun  7201  fliftf  7271  imaeqsexvOLD  7319  imaeqexov  7606  fiun  7897  f1iun  7898  oprabrexex2  7932  releldm2  7997  oarec  8499  omeu  8522  eroveu  8761  brttrcl2  9635  dfac5lem2  10046  genpass  10932  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  pceu  16786  4sqlem12  16896  mreiincl  17527  psgneu  19447  ntreq0  23033  unisngl  23483  metrest  24480  metuel2  24521  nosupno  27683  nosupfv  27686  noinfno  27698  noinffv  27701  elold  27867  lrrecfr  27951  leadds1  27997  addsuniflem  28009  addsasslem1  28011  addsasslem2  28012  mulsuniflem  28157  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  elreno2  28503  renegscl  28506  readdscl  28507  remulscl  28510  istrkg2ld  28544  fpwrelmapffslem  32821  omssubaddlem  34476  omssubadd  34477  bnj906  35105  satfdm  35582  dmopab3rexdif  35618  rexxfr3dALT  35852  bj-elsngl  37207  bj-restn0  37334  ismblfin  37901  itg2addnclem3  37913  sdclem1  37983  eldmqs1cossres  38984  prter2  39246  lshpsmreu  39474  islpln5  39900  islvol5  39944  cdlemftr3  40930  mapdpglem3  42040  hdmapglem7a  42292  diophrex  43121  imaiun1  43996  coiun1  43997  grumnudlem  44630  upbdrech  45656  usgrgrtrirex  48299