Theorem rexcom4 3234

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1782   ∈ wcel 2107  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-11 2155

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  2ex2rexrot  3236  rexcom4a  3237  rexcomOLD  3286  reuind  3689  uni0b  4868  iuncom4  4933  dfiun2g  4961  dfiun2gOLD  4962  iunn0  4997  iunxiun  5027  iinexg  5266  inuni  5268  iunopab  5473  iunopabOLD  5474  xpiundi  5658  xpiundir  5659  cnvuni  5798  dmiun  5825  dmopab2rex  5829  elsnres  5934  rniun  6056  xpdifid  6076  imaco  6159  coiun  6164  abrexco  7126  imaiun  7127  fliftf  7195  fiun  7794  f1iun  7795  oprabrexex2  7830  releldm2  7893  oarec  8402  omeu  8425  eroveu  8610  brttrcl2  9481  dfac5lem2  9889  genpass  10774  supaddc  11951  supadd  11952  supmul1  11953  supmullem2  11955  supmul  11956  pceu  16556  4sqlem12  16666  mreiincl  17314  psgneu  19123  ntreq0  22237  unisngl  22687  metrest  23689  metuel2  23730  istrkg2ld  26830  fpwrelmapffslem  31076  omssubaddlem  32275  omssubadd  32276  bnj906  32919  satfdm  33340  dmopab3rexdif  33376  imaeqsexv  33699  nosupno  33915  nosupfv  33918  noinfno  33930  noinffv  33933  elold  34062  lrrecfr  34109  bj-elsngl  35167  bj-restn0  35270  ismblfin  35827  itg2addnclem3  35839  sdclem1  35910  eldmqs1cossres  36778  prter2  36902  lshpsmreu  37130  islpln5  37556  islvol5  37600  cdlemftr3  38586  mapdpglem3  39696  hdmapglem7a  39948  diophrex  40604  imaiun1  41266  coiun1  41267  grumnudlem  41910  upbdrech  42851