Theorem rexcom4 3267

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 1961	. 2 ⊢ (∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
2		df-rex 3065	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
3	2	exbii 1855	. . 3 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		excom 2173	. . 3 ⊢ (∃𝑦∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
5	3, 4	bitri 276	. 2 ⊢ (∃𝑦∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥∃𝑦(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦𝜑))
7	1, 5, 6	3bitr4ri 305	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-11 2168

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexcom4a  3270  2ex2rexrot  3275  reuind  3701  uni0b  4871  iuncom4  4937  dfiun2g  4966  iunn0  5003  iunxiun  5033  iinexg  5283  inuni  5285  iunopab  5508  xpiundi  5696  xpiundir  5697  cnvuni  5835  dmiun  5862  dmopab2rex  5866  elsnres  5980  rniun  6105  xpdifid  6126  imaco  6209  coiun  6215  abrexco  7195  imaiun  7196  fliftf  7266  imaeqsexvOLD  7314  imaeqexov  7601  fiun  7892  f1iun  7893  oprabrexex2  7927  releldm2  7992  oarec  8494  omeu  8517  eroveu  8756  brttrcl2  9633  dfac5lem2  10044  genpass  10930  supaddc  12121  supadd  12122  supmul1  12123  supmullem2  12125  supmul  12126  pceu  16815  4sqlem12  16925  mreiincl  17556  psgneu  19479  ntreq0  23067  unisngl  23517  metrest  24514  metuel2  24555  nosupno  27692  nosupfv  27695  noinfno  27707  noinffv  27710  elold  27876  lrrecfr  27960  leadds1  28006  addsuniflem  28018  addsasslem1  28020  addsasslem2  28021  mulsuniflem  28166  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  elreno2  28512  renegscl  28515  readdscl  28516  remulscl  28519  istrkg2ld  28553  fpwrelmapffslem  32831  omssubaddlem  34490  omssubadd  34491  bnj906  35119  satfdm  35598  dmopab3rexdif  35634  rexxfr3dALT  35868  bj-elsngl  37322  bj-restn0  37449  ismblfin  38029  itg2addnclem3  38041  sdclem1  38111  eldmqs1cossres  39112  prter2  39374  lshpsmreu  39602  islpln5  40028  islvol5  40072  cdlemftr3  41058  mapdpglem3  42168  hdmapglem7a  42420  diophrex  43225  imaiun1  44096  coiun1  44097  grumnudlem  44730  upbdrech  45754  usgrgrtrirex  48442