MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexcom4 Structured version   Unicode version

Theorem rexcom4 3004
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  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Distinct variable groups:    x, y    y, A
Allowed substitution hints:    ph( x, y)    A( x)

Proof of Theorem rexcom4
StepHypRef Expression
1 rexcom 2894 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2999 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2752 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2999 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 275 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1586   E.wrex 2728   _Vcvv 2984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2733  df-v 2986
This theorem is referenced by:  rexcom4a  3005  reuind  3174  uni0b  4128  iuncom4  4190  dfiun2g  4214  iunn0  4242  iunxiun  4265  iinexg  4464  inuni  4466  iunopab  4636  xpiundi  4905  xpiundir  4906  cnvuni  5038  dmiun  5060  elres  5157  elsnres  5158  rniun  5259  xpdifid  5278  imaco  5355  coiun  5359  abrexco  5973  imaiun  5974  fliftf  6020  fun11iun  6549  oprabrexex2  6579  releldm2  6636  oarec  7013  omeu  7036  eroveu  7207  dfac5lem2  8306  genpass  9190  supmul1  10307  supmullem2  10309  supmul  10310  pceu  13925  4sqlem12  14029  mreiincl  14546  psgneu  16024  ntreq0  18693  metrest  20111  metuel2  20166  fpwrelmapffslem  26044  nofulllem5  27859  supaddc  28429  supadd  28430  ismblfin  28444  itg2addnclem3  28457  sdclem1  28651  prter2  29038  diophrex  29126  el2wlkonot  30400  el2spthonot  30401  el2wlkonotot0  30403  bnj906  31935  bj-elsngl  32473  lshpsmreu  32766  islpln5  33191  islvol5  33235  cdlemftr3  34221  mapdpglem3  35332  hdmapglem7a  35587
  Copyright terms: Public domain W3C validator