Theorem rexcom4 3427

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 3285	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑)
2		rexv 3422	. . 3 ⊢ (∃𝑦 ∈ V 𝜑 ↔ ∃𝑦𝜑)
3	2	rexbii 3224	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ V 𝜑 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦𝜑)
4		rexv 3422	. 2 ⊢ (∃𝑦 ∈ V ∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)
5	1, 3, 4	3bitr3i 293	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦𝜑 ↔ ∃𝑦∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   ↔ wb 198  ∃wex 1823  ∃wrex 3091  Vcvv 3398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-v 3400

This theorem is referenced by:  rexcom4a  3428  reuind  3628  uni0b  4698  iuncom4  4761  dfiun2g  4785  iunn0  4813  iunxiun  4842  iinexg  5058  inuni  5060  iunopab  5249  xpiundi  5419  xpiundir  5420  cnvuni  5554  dmiun  5578  elresOLD  5685  elsnres  5686  rniun  5797  xpdifid  5816  imaco  5894  coiun  5899  abrexco  6774  imaiun  6775  fliftf  6837  fun11iun  7405  oprabrexex2  7435  releldm2  7497  oarec  7926  omeu  7949  eroveu  8126  dfac5lem2  9280  genpass  10166  supaddc  11344  supadd  11345  supmul1  11346  supmullem2  11348  supmul  11349  pceu  15955  4sqlem12  16064  mreiincl  16642  psgneu  18310  ntreq0  21289  unisngl  21739  metrest  22737  metuel2  22778  istrkg2ld  25811  fpwrelmapffslem  30073  omssubaddlem  30959  omssubadd  30960  bnj906  31599  nosupno  32438  nosupfv  32441  bj-elsngl  33528  bj-restn0  33616  ismblfin  34078  itg2addnclem3  34090  sdclem1  34165  prter2  35037  lshpsmreu  35265  islpln5  35691  islvol5  35735  cdlemftr3  36721  mapdpglem3  37831  hdmapglem7a  38083  diophrex  38303  imaiun1  38904  coiun1  38905  upbdrech  40432