Theorem rexcom4 3179

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 1959	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3069	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1851	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2164	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 274	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 303	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 205   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-11 2156

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  2ex2rexrot  3180  rexcom4a  3181  rexcom  3281  reuind  3683  uni0b  4864  iuncom4  4929  dfiun2g  4957  iunn0  4992  iunxiun  5022  iinexg  5260  inuni  5262  iunopab  5465  xpiundi  5648  xpiundir  5649  cnvuni  5784  dmiun  5811  dmopab2rex  5815  elsnres  5920  rniun  6040  xpdifid  6060  imaco  6144  coiun  6149  abrexco  7099  imaiun  7100  fliftf  7166  fiun  7759  f1iun  7760  oprabrexex2  7794  releldm2  7857  oarec  8355  omeu  8378  eroveu  8559  dfac5lem2  9811  genpass  10696  supaddc  11872  supadd  11873  supmul1  11874  supmullem2  11876  supmul  11877  pceu  16475  4sqlem12  16585  mreiincl  17222  psgneu  19029  ntreq0  22136  unisngl  22586  metrest  23586  metuel2  23627  istrkg2ld  26725  fpwrelmapffslem  30969  omssubaddlem  32166  omssubadd  32167  bnj906  32810  satfdm  33231  dmopab3rexdif  33267  imaeqsexv  33593  brttrcl2  33700  nosupno  33833  nosupfv  33836  noinfno  33848  noinffv  33851  elold  33980  lrrecfr  34027  bj-elsngl  35085  bj-restn0  35188  ismblfin  35745  itg2addnclem3  35757  sdclem1  35828  eldmqs1cossres  36698  prter2  36822  lshpsmreu  37050  islpln5  37476  islvol5  37520  cdlemftr3  38506  mapdpglem3  39616  hdmapglem7a  39868  diophrex  40513  imaiun1  41148  coiun1  41149  grumnudlem  41792  upbdrech  42734