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  3700  uni0b  4877  iuncom4  4943  dfiun2g  4973  iunn0  5010  iunxiun  5040  iinexg  5290  inuni  5292  iunopab  5514  xpiundi  5702  xpiundir  5703  cnvuni  5842  dmiun  5869  dmopab2rex  5873  elsnres  5987  rniun  6112  xpdifid  6133  imaco  6216  coiun  6222  abrexco  7199  imaiun  7200  fliftf  7270  imaeqsexvOLD  7318  imaeqexov  7605  fiun  7896  f1iun  7897  oprabrexex2  7931  releldm2  7996  oarec  8497  omeu  8520  eroveu  8759  brttrcl2  9635  dfac5lem2  10046  genpass  10932  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  pceu  16817  4sqlem12  16927  mreiincl  17558  psgneu  19481  ntreq0  23042  unisngl  23492  metrest  24489  metuel2  24530  nosupno  27667  nosupfv  27670  noinfno  27682  noinffv  27685  elold  27851  lrrecfr  27935  leadds1  27981  addsuniflem  27993  addsasslem1  27995  addsasslem2  27996  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  elreno2  28487  renegscl  28490  readdscl  28491  remulscl  28494  istrkg2ld  28528  fpwrelmapffslem  32805  omssubaddlem  34443  omssubadd  34444  bnj906  35072  satfdm  35551  dmopab3rexdif  35587  rexxfr3dALT  35821  bj-elsngl  37275  bj-restn0  37402  ismblfin  37982  itg2addnclem3  37994  sdclem1  38064  eldmqs1cossres  39065  prter2  39327  lshpsmreu  39555  islpln5  39981  islvol5  40025  cdlemftr3  41011  mapdpglem3  42121  hdmapglem7a  42373  diophrex  43207  imaiun1  44078  coiun1  44079  grumnudlem  44712  upbdrech  45738  usgrgrtrirex  48420