Theorem rexcom4 3264

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-11 2158

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexcom4a  3267  2ex2rexrot  3273  reuind  3724  uni0b  4897  iuncom4  4964  dfiun2g  4994  dfiun2gOLD  4995  iunn0  5031  iunxiun  5061  iinexg  5303  inuni  5305  iunopab  5519  iunopabOLD  5520  xpiundi  5709  xpiundir  5710  cnvuni  5850  dmiun  5877  dmopab2rex  5881  elsnres  5992  rniun  6120  xpdifid  6141  imaco  6224  coiun  6229  abrexco  7218  imaiun  7219  fliftf  7290  imaeqsexvOLD  7338  imaeqexov  7627  fiun  7921  f1iun  7922  oprabrexex2  7957  releldm2  8022  oarec  8526  omeu  8549  eroveu  8785  brttrcl2  9667  dfac5lem2  10077  genpass  10962  supaddc  12150  supadd  12151  supmul1  12152  supmullem2  12154  supmul  12155  pceu  16817  4sqlem12  16927  mreiincl  17557  psgneu  19436  ntreq0  22964  unisngl  23414  metrest  24412  metuel2  24453  nosupno  27615  nosupfv  27618  noinfno  27630  noinffv  27633  elold  27781  lrrecfr  27850  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  renegscl  28349  readdscl  28350  remulscl  28353  istrkg2ld  28387  fpwrelmapffslem  32655  omssubaddlem  34290  omssubadd  34291  bnj906  34920  satfdm  35356  dmopab3rexdif  35392  rexxfr3dALT  35626  bj-elsngl  36956  bj-restn0  37078  ismblfin  37655  itg2addnclem3  37667  sdclem1  37737  eldmqs1cossres  38651  prter2  38874  lshpsmreu  39102  islpln5  39529  islvol5  39573  cdlemftr3  40559  mapdpglem3  41669  hdmapglem7a  41921  diophrex  42763  imaiun1  43640  coiun1  43641  grumnudlem  44274  upbdrech  45303  usgrgrtrirex  47949