Theorem rexcom4 3257

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2110  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-11 2159

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3055

This theorem is referenced by:  rexcom4a  3260  2ex2rexrot  3265  reuind  3710  uni0b  4883  iuncom4  4948  dfiun2g  4978  iunn0  5013  iunxiun  5043  iinexg  5284  inuni  5286  iunopab  5497  xpiundi  5685  xpiundir  5686  cnvuni  5824  dmiun  5851  dmopab2rex  5855  elsnres  5967  rniun  6091  xpdifid  6112  imaco  6195  coiun  6200  abrexco  7173  imaiun  7174  fliftf  7244  imaeqsexvOLD  7292  imaeqexov  7579  fiun  7870  f1iun  7871  oprabrexex2  7905  releldm2  7970  oarec  8472  omeu  8495  eroveu  8731  brttrcl2  9599  dfac5lem2  10007  genpass  10892  supaddc  12081  supadd  12082  supmul1  12083  supmullem2  12085  supmul  12086  pceu  16750  4sqlem12  16860  mreiincl  17490  psgneu  19411  ntreq0  22985  unisngl  23435  metrest  24432  metuel2  24473  nosupno  27635  nosupfv  27638  noinfno  27650  noinffv  27653  elold  27807  lrrecfr  27879  sleadd1  27925  addsuniflem  27937  addsasslem1  27939  addsasslem2  27940  mulsuniflem  28081  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  renegscl  28393  readdscl  28394  remulscl  28397  istrkg2ld  28431  fpwrelmapffslem  32705  omssubaddlem  34302  omssubadd  34303  bnj906  34932  satfdm  35381  dmopab3rexdif  35417  rexxfr3dALT  35651  bj-elsngl  36981  bj-restn0  37103  ismblfin  37680  itg2addnclem3  37692  sdclem1  37762  eldmqs1cossres  38676  prter2  38899  lshpsmreu  39127  islpln5  39553  islvol5  39597  cdlemftr3  40583  mapdpglem3  41693  hdmapglem7a  41945  diophrex  42787  imaiun1  43663  coiun1  43664  grumnudlem  44297  upbdrech  45325  usgrgrtrirex  47960