Theorem rexcom4 3285

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-11 2154

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexcomOLD  3288  rexcom4a  3289  2ex2rexrot  3295  reuind  3761  uni0b  4937  iuncom4  5004  dfiun2g  5034  dfiun2gOLD  5035  iunn0  5071  iunxiun  5101  iinexg  5353  inuni  5355  iunopab  5568  iunopabOLD  5569  xpiundi  5758  xpiundir  5759  cnvuni  5899  dmiun  5926  dmopab2rex  5930  elsnres  6040  rniun  6169  xpdifid  6189  imaco  6272  coiun  6277  abrexco  7263  imaiun  7264  fliftf  7334  imaeqsexvOLD  7382  imaeqexov  7670  fiun  7965  f1iun  7966  oprabrexex2  8001  releldm2  8066  oarec  8598  omeu  8621  eroveu  8850  brttrcl2  9751  dfac5lem2  10161  genpass  11046  supaddc  12232  supadd  12233  supmul1  12234  supmullem2  12236  supmul  12237  pceu  16879  4sqlem12  16989  mreiincl  17640  psgneu  19538  ntreq0  23100  unisngl  23550  metrest  24552  metuel2  24593  nosupno  27762  nosupfv  27765  noinfno  27777  noinffv  27780  elold  27922  lrrecfr  27990  sleadd1  28036  addsuniflem  28048  addsasslem1  28050  addsasslem2  28051  mulsuniflem  28189  addsdilem1  28191  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  renegscl  28444  readdscl  28445  remulscl  28448  istrkg2ld  28482  fpwrelmapffslem  32749  omssubaddlem  34280  omssubadd  34281  bnj906  34922  satfdm  35353  dmopab3rexdif  35389  rexxfr3dALT  35623  bj-elsngl  36950  bj-restn0  37072  ismblfin  37647  itg2addnclem3  37659  sdclem1  37729  eldmqs1cossres  38640  prter2  38862  lshpsmreu  39090  islpln5  39517  islvol5  39561  cdlemftr3  40547  mapdpglem3  41657  hdmapglem7a  41909  diophrex  42762  imaiun1  43640  coiun1  43641  grumnudlem  44280  upbdrech  45255  usgrgrtrirex  47852