Theorem rexcom4 3291

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400  ∃wex 1808   ∈ wcel 2142  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-11 2191

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-rex 3089

This theorem is used by:  rexcom4a  3294  2ex2rexrot  3299  reuind  3715  uni0b  4898  iuncom4  4964  dfiun2g  4993  iunn0  5030  iunxiun  5062  iinexg  5317  inuni  5319  iunopab  5543  xpiundi  5731  xpiundir  5732  cnvuni  5875  dmiun  5902  dmopab2rex  5906  elsnres  6019  rniun  6144  xpdifid  6164  xpdifcnvepel  6165  imaco  6251  coiun  6257  abrexco  7242  imaiun  7243  fliftf  7313  imaeqsexvOLD  7363  imaeqexov  7650  fiun  7938  f1iun  7939  oprabrexex2  7973  releldm2  8038  oarec  8545  omeu  8568  eroveu  8808  brttrcl2  9681  dfac5lem2  10115  genpass  11000  supaddc  12188  supadd  12189  supmul1  12190  supmullem2  12192  supmul  12193  pceu  16912  4sqlem12  17022  mreiincl  17654  psgneu  19582  ntreq0  23245  unisngl  23695  metrest  24692  metuel2  24733  nosupno  27878  nosupfv  27881  noinfno  27893  noinffv  27896  elold  28063  lrrecfr  28147  leadds1  28193  addsuniflem  28205  addsasslem1  28207  addsasslem2  28208  mulsuniflem  28353  addsdilem1  28355  addsdilem2  28356  mulsasslem1  28367  mulsasslem2  28368  elreno2  28699  renegscl  28702  readdscl  28703  remulscl  28706  istrkg2ld  28740  fpwrelmapffslem  33088  omssubaddlem  34698  omssubadd  34699  bnj906  35327  satfdm  35869  dmopab3rexdif  35905  rexxfr3dALT  36139  bj-elsngl  37632  bj-restn0  37760  ismblfin  38340  itg2addnclem3  38352  sdclem1  38422  eldmqs1cossres  39421  prter2  39683  lshpsmreu  39911  islpln5  40337  islvol5  40381  cdlemftr3  41367  mapdpglem3  42477  hdmapglem7a  42729  diophrex  43534  imaiun1  44405  coiun1  44406  grumnudlem  45023  upbdrech  46052  usgrgrtrirex  48743