Theorem rexcom4 3290

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1807   ∈ wcel 2141  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-11 2190

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-rex 3088

This theorem is referenced by:  rexcom4a  3293  2ex2rexrot  3298  reuind  3715  uni0b  4898  iuncom4  4964  dfiun2g  4993  iunn0  5030  iunxiun  5062  iinexg  5318  inuni  5320  iunopab  5544  xpiundi  5732  xpiundir  5733  cnvuni  5876  dmiun  5903  dmopab2rex  5907  elsnres  6020  rniun  6145  xpdifid  6165  xpdifcnvepel  6166  imaco  6252  coiun  6258  abrexco  7242  imaiun  7243  fliftf  7313  imaeqsexvOLD  7361  imaeqexov  7648  fiun  7939  f1iun  7940  oprabrexex2  7974  releldm2  8039  oarec  8546  omeu  8569  eroveu  8809  brttrcl2  9682  dfac5lem2  10107  genpass  10993  supaddc  12181  supadd  12182  supmul1  12183  supmullem2  12185  supmul  12186  pceu  16905  4sqlem12  17015  mreiincl  17647  psgneu  19575  ntreq0  23213  unisngl  23663  metrest  24660  metuel2  24701  nosupno  27843  nosupfv  27846  noinfno  27858  noinffv  27861  elold  28028  lrrecfr  28112  leadds1  28158  addsuniflem  28170  addsasslem1  28172  addsasslem2  28173  mulsuniflem  28318  addsdilem1  28320  addsdilem2  28321  mulsasslem1  28332  mulsasslem2  28333  elreno2  28664  renegscl  28667  readdscl  28668  remulscl  28671  istrkg2ld  28705  fpwrelmapffslem  33043  omssubaddlem  34655  omssubadd  34656  bnj906  35284  satfdm  35827  dmopab3rexdif  35863  rexxfr3dALT  36097  bj-elsngl  37570  bj-restn0  37698  ismblfin  38278  itg2addnclem3  38290  sdclem1  38360  eldmqs1cossres  39361  prter2  39623  lshpsmreu  39851  islpln5  40277  islvol5  40321  cdlemftr3  41307  mapdpglem3  42417  hdmapglem7a  42669  diophrex  43476  imaiun1  44347  coiun1  44348  grumnudlem  44965  upbdrech  45994  usgrgrtrirex  48682