Theorem rexcom4 3293

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

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

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 1945  ax-11 2197

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  rexcom4a  3296  2ex2rexrot  3301  reuind  3714  uni0b  4897  iuncom4  4963  dfiun2g  4991  iunn0  5028  iunxiun  5060  iinexg  5313  inuni  5315  iunopab  5538  xpiundi  5726  xpiundir  5727  cnvuni  5875  dmiun  5902  dmopab2rex  5906  elsnres  6022  rniun  6151  xpdifid  6171  xpdifcnvepel  6172  imaco  6265  coiun  6271  abrexco  7271  imaiun  7272  fliftf  7346  imaeqexov  7683  fiun  7979  f1iun  7980  oprabrexex2  8014  releldm2  8078  oarec  8598  omeu  8621  eroveu  8861  brttrcl2  9742  dfac5lem2  10230  genpass  11121  supaddc  12311  supadd  12312  supmul1  12313  supmullem2  12315  supmul  12316  pceu  17053  4sqlem12  17163  mreiincl  17795  psgneu  19750  ntreq0  23425  unisngl  23876  metrest  24873  metuel2  24914  nosupno  28090  nosupfv  28093  noinfno  28105  noinffv  28108  elold  28275  lrrecfr  28359  leadds1  28405  addsuniflem  28417  addsasslem1  28419  addsasslem2  28420  mulsuniflem  28565  addsdilem1  28567  addsdilem2  28568  mulsasslem1  28579  mulsasslem2  28580  elreno2  28911  renegscl  28914  readdscl  28915  remulscl  28918  istrkg2ld  28952  fpwrelmapffslem  33394  omssubaddlem  35001  omssubadd  35002  bnj906  35630  satfdm  36301  dmopab3rexdif  36337  rexxfr3dALT  36571  bj-elsngl  38059  bj-restn0  38202  ismblfin  38771  itg2addnclem3  38783  sdclem1  38869  eldmqs1cossres  39868  prter2  40130  lshpsmreu  40358  islpln5  40784  islvol5  40828  cdlemftr3  41814  mapdpglem3  42924  hdmapglem7a  43176  diophrex  43979  imaiun1  44843  coiun1  44844  grumnudlem  45461  upbdrech  46526  usgrgrtrirex  49253