Theorem rexcom4 3261

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3058

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 2162

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

This theorem is referenced by:  rexcom4a  3264  2ex2rexrot  3269  reuind  3709  uni0b  4886  iuncom4  4952  dfiun2g  4982  iunn0  5019  iunxiun  5049  iinexg  5290  inuni  5292  iunopab  5504  xpiundi  5692  xpiundir  5693  cnvuni  5833  dmiun  5860  dmopab2rex  5864  elsnres  5977  rniun  6102  xpdifid  6123  imaco  6206  coiun  6212  abrexco  7187  imaiun  7188  fliftf  7258  imaeqsexvOLD  7306  imaeqexov  7593  fiun  7884  f1iun  7885  oprabrexex2  7919  releldm2  7984  oarec  8486  omeu  8509  eroveu  8745  brttrcl2  9614  dfac5lem2  10025  genpass  10910  supaddc  12099  supadd  12100  supmul1  12101  supmullem2  12103  supmul  12104  pceu  16768  4sqlem12  16878  mreiincl  17508  psgneu  19428  ntreq0  23002  unisngl  23452  metrest  24449  metuel2  24490  nosupno  27652  nosupfv  27655  noinfno  27667  noinffv  27670  elold  27824  lrrecfr  27896  sleadd1  27942  addsuniflem  27954  addsasslem1  27956  addsasslem2  27957  mulsuniflem  28098  addsdilem1  28100  addsdilem2  28101  mulsasslem1  28112  mulsasslem2  28113  renegscl  28410  readdscl  28411  remulscl  28414  istrkg2ld  28448  fpwrelmapffslem  32726  omssubaddlem  34323  omssubadd  34324  bnj906  34953  satfdm  35424  dmopab3rexdif  35460  rexxfr3dALT  35694  bj-elsngl  37023  bj-restn0  37145  ismblfin  37711  itg2addnclem3  37723  sdclem1  37793  eldmqs1cossres  38767  prter2  38990  lshpsmreu  39218  islpln5  39644  islvol5  39688  cdlemftr3  40674  mapdpglem3  41784  hdmapglem7a  42036  diophrex  42882  imaiun1  43758  coiun1  43759  grumnudlem  44392  upbdrech  45420  usgrgrtrirex  48064