Theorem rexcom4 3289

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-11 2194

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rexcom4a  3292  2ex2rexrot  3297  reuind  3710  uni0b  4893  iuncom4  4959  dfiun2g  4987  iunn0  5024  iunxiun  5056  iinexg  5308  inuni  5310  iunopab  5530  xpiundi  5718  xpiundir  5719  cnvuni  5864  dmiun  5891  dmopab2rex  5895  elsnres  6008  rniun  6133  xpdifid  6154  xpdifcnvepel  6155  imaco  6241  coiun  6247  abrexco  7236  imaiun  7237  fliftf  7311  imaeqexov  7647  fiun  7938  f1iun  7939  oprabrexex2  7973  releldm2  8037  oarec  8548  omeu  8571  eroveu  8811  brttrcl2  9693  dfac5lem2  10175  genpass  11066  supaddc  12254  supadd  12255  supmul1  12256  supmullem2  12258  supmul  12259  pceu  16986  4sqlem12  17096  mreiincl  17728  psgneu  19682  ntreq0  23357  unisngl  23808  metrest  24805  metuel2  24846  nosupno  27994  nosupfv  27997  noinfno  28009  noinffv  28012  elold  28179  lrrecfr  28263  leadds1  28309  addsuniflem  28321  addsasslem1  28323  addsasslem2  28324  mulsuniflem  28469  addsdilem1  28471  addsdilem2  28472  mulsasslem1  28483  mulsasslem2  28484  elreno2  28815  renegscl  28818  readdscl  28819  remulscl  28822  istrkg2ld  28856  fpwrelmapffslem  33258  omssubaddlem  34866  omssubadd  34867  bnj906  35495  satfdm  36055  dmopab3rexdif  36091  rexxfr3dALT  36325  bj-elsngl  37803  bj-restn0  37931  ismblfin  38499  itg2addnclem3  38511  sdclem1  38597  eldmqs1cossres  39596  prter2  39858  lshpsmreu  40086  islpln5  40512  islvol5  40556  cdlemftr3  41542  mapdpglem3  42652  hdmapglem7a  42904  diophrex  43724  imaiun1  44595  coiun1  44596  grumnudlem  45213  upbdrech  46242  usgrgrtrirex  48970