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

Theorem rexcom4 2975
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 2869 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2970 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2730 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2970 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 267 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550   E.wrex 2706   _Vcvv 2956
This theorem is referenced by:  rexcom4a  2976  reuind  3137  uni0b  4040  iuncom4  4100  dfiun2g  4123  iunn0  4151  iunxiun  4173  iinexg  4360  inuni  4362  iunopab  4486  xpiundi  4932  xpiundir  4933  cnvuni  5057  dmiun  5078  elres  5181  elsnres  5182  rniun  5282  imaco  5375  coiun  5379  fun11iun  5695  abrexco  5986  imaiun  5992  fliftf  6037  oprabrexex2  6189  releldm2  6397  oarec  6805  omeu  6828  eroveu  6999  dfac5lem2  8005  genpass  8886  supmul1  9973  supmullem2  9975  supmul  9976  pceu  13220  4sqlem12  13324  mreiincl  13821  ntreq0  17141  metrest  18554  metuel2  18609  nofulllem5  25661  supaddc  26237  supadd  26238  ismblfin  26247  itg2addnclem3  26258  sdclem1  26447  prter2  26730  diophrex  26834  psgneu  27406  el2wlkonot  28336  el2spthonot  28337  el2wlkonotot0  28339  bnj906  29301  lshpsmreu  29907  islpln5  30332  islvol5  30376  cdlemftr3  31362  mapdpglem3  32473  hdmapglem7a  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-v 2958
  Copyright terms: Public domain W3C validator