Theorem rexcom4 3198

Description: Commutation of restricted and unrestricted existential quantifiers. (Contributed by NM, 12-Apr-2004.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)

Assertion

Ref	Expression
rexcom4	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)

Proof of Theorem rexcom4

Step	Hyp	Ref	Expression
1		rexcom 3080	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑)
2		rexv 3193	. . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
3	2	rexbii 3023	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑)
4		rexv 3193	. 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
5	1, 3, 4	3bitr3i 289	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 195  ∃wex 1695  ∃wrex 2897  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175

This theorem is referenced by:  rexcom4a  3199  reuind  3378  uni0b  4399  iuncom4  4464  dfiun2g  4488  iunn0  4516  iunxiun  4544  iinexg  4751  inuni  4753  iunopab  4936  xpiundi  5096  xpiundir  5097  cnvuni  5231  dmiun  5255  elres  5355  elsnres  5356  rniun  5462  xpdifid  5481  imaco  5557  coiun  5562  abrexco  6406  imaiun  6407  fliftf  6465  fun11iun  7019  oprabrexex2  7049  releldm2  7109  oarec  7529  omeu  7552  eroveu  7729  dfac5lem2  8830  genpass  9710  supaddc  10867  supadd  10868  supmul1  10869  supmullem2  10871  supmul  10872  pceu  15389  4sqlem12  15498  mreiincl  16079  psgneu  17749  ntreq0  20691  unisngl  21140  metrest  22139  metuel2  22180  istrkg2ld  25159  el2wlkonot  26396  el2spthonot  26397  el2wlkonotot0  26399  fpwrelmapffslem  28895  omssubaddlem  29688  omssubadd  29689  bnj906  30254  nofulllem5  31105  bj-elsngl  32149  bj-restn0  32224  ismblfin  32620  itg2addnclem3  32633  sdclem1  32709  prter2  33184  lshpsmreu  33414  islpln5  33839  islvol5  33883  cdlemftr3  34871  mapdpglem3  35982  hdmapglem7a  36237  diophrex  36357  imaiun1  36962  coiun1  36963  upbdrech  38460