Theorem rexcom4 3291

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

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

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 3089

This theorem is used by:  rexcom4a  3294  2ex2rexrot  3299  reuind  3714  uni0b  4897  iuncom4  4963  dfiun2g  4992  iunn0  5029  iunxiun  5061  iinexg  5316  inuni  5318  iunopab  5542  xpiundi  5730  xpiundir  5731  cnvuni  5874  dmiun  5901  dmopab2rex  5905  elsnres  6018  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  imaco  6251  coiun  6257  abrexco  7244  imaiun  7245  fliftf  7319  imaeqexov  7655  fiun  7943  f1iun  7944  oprabrexex2  7978  releldm2  8043  oarec  8552  omeu  8575  eroveu  8815  brttrcl2  9696  dfac5lem2  10130  genpass  11021  supaddc  12209  supadd  12210  supmul1  12211  supmullem2  12213  supmul  12214  pceu  16942  4sqlem12  17052  mreiincl  17684  psgneu  19637  ntreq0  23306  unisngl  23757  metrest  24754  metuel2  24795  nosupno  27940  nosupfv  27943  noinfno  27955  noinffv  27958  elold  28125  lrrecfr  28209  leadds1  28255  addsuniflem  28267  addsasslem1  28269  addsasslem2  28270  mulsuniflem  28415  addsdilem1  28417  addsdilem2  28418  mulsasslem1  28429  mulsasslem2  28430  elreno2  28761  renegscl  28764  readdscl  28765  remulscl  28768  istrkg2ld  28802  fpwrelmapffslem  33205  omssubaddlem  34812  omssubadd  34813  bnj906  35441  satfdm  35950  dmopab3rexdif  35986  rexxfr3dALT  36220  bj-elsngl  37714  bj-restn0  37842  ismblfin  38412  itg2addnclem3  38424  sdclem1  38495  eldmqs1cossres  39494  prter2  39756  lshpsmreu  39984  islpln5  40410  islvol5  40454  cdlemftr3  41440  mapdpglem3  42550  hdmapglem7a  42802  diophrex  43622  imaiun1  44493  coiun1  44494  grumnudlem  45111  upbdrech  46140  usgrgrtrirex  48868