Theorem rexcom4 3283

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 1968	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3081	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1862	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2190	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 277	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3081	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 306	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1793   ∈ wcel 2136  ∃wrex 3080

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-11 2185

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1794  df-rex 3081

This theorem is referenced by:  rexcom4a  3286  2ex2rexrot  3291  reuind  3710  uni0b  4886  iuncom4  4952  dfiun2g  4981  iunn0  5018  iunxiun  5048  iinexg  5298  inuni  5300  iunopab  5523  xpiundi  5711  xpiundir  5712  cnvuni  5855  dmiun  5882  dmopab2rex  5886  elsnres  6000  rniun  6122  xpdifid  6143  imaco  6227  coiun  6233  abrexco  7217  imaiun  7218  fliftf  7288  imaeqsexvOLD  7336  imaeqexov  7623  fiun  7913  f1iun  7914  oprabrexex2  7948  releldm2  8013  oarec  8519  omeu  8542  eroveu  8782  brttrcl2  9659  dfac5lem2  10070  genpass  10957  supaddc  12149  supadd  12150  supmul1  12151  supmullem2  12153  supmul  12154  pceu  16858  4sqlem12  16968  mreiincl  17600  psgneu  19522  ntreq0  23110  unisngl  23560  metrest  24557  metuel2  24598  nosupno  27737  nosupfv  27740  noinfno  27752  noinffv  27755  elold  27922  lrrecfr  28006  leadds1  28052  addsuniflem  28064  addsasslem1  28066  addsasslem2  28067  mulsuniflem  28212  addsdilem1  28214  addsdilem2  28215  mulsasslem1  28226  mulsasslem2  28227  elreno2  28558  renegscl  28561  readdscl  28562  remulscl  28565  istrkg2ld  28599  fpwrelmapffslem  32877  omssubaddlem  34550  omssubadd  34551  bnj906  35182  satfdm  35667  dmopab3rexdif  35703  rexxfr3dALT  35937  bj-elsngl  37401  bj-restn0  37528  ismblfin  38108  itg2addnclem3  38120  sdclem1  38190  eldmqs1cossres  39191  prter2  39453  lshpsmreu  39681  islpln5  40107  islvol5  40151  cdlemftr3  41137  mapdpglem3  42247  hdmapglem7a  42499  diophrex  43304  imaiun1  44175  coiun1  44176  grumnudlem  44809  upbdrech  45832  usgrgrtrirex  48520