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

Theorem rexcom4 2807
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 2701 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2802 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2568 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2802 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 266 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528   E.wrex 2544   _Vcvv 2788
This theorem is referenced by:  rexcom4a  2808  reuind  2968  uni0b  3852  iuncom4  3912  dfiun2g  3935  iunn0  3962  iunxiun  3984  iinexg  4171  inuni  4173  iunopab  4296  xpiundi  4743  xpiundir  4744  cnvuni  4866  dmiun  4887  elres  4990  elsnres  4991  rniun  5091  imaco  5178  coiun  5182  fun11iun  5493  abrexco  5766  imaiun  5771  fliftf  5814  oprabrexex2  5963  releldm2  6170  oarec  6560  omeu  6583  eroveu  6753  dfac5lem2  7751  genpass  8633  supmul1  9719  supmullem2  9721  supmul  9722  pceu  12899  4sqlem12  13003  mreiincl  13498  ntreq0  16814  metrest  18070  nofulllem5  24360  elfuns  24454  sdclem1  26453  prter2  26749  diophrex  26855  psgneu  27429  bnj906  28962  lshpsmreu  29299  islpln5  29724  islvol5  29768  cdlemftr3  30754  mapdpglem3  31865  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790
  Copyright terms: Public domain W3C validator