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

Theorem rexcom4 2820
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 2714 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 2815 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2581 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 2815 . 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 1531   E.wrex 2557   _Vcvv 2801
This theorem is referenced by:  rexcom4a  2821  reuind  2981  uni0b  3868  iuncom4  3928  dfiun2g  3951  iunn0  3978  iunxiun  4000  iinexg  4187  inuni  4189  iunopab  4312  xpiundi  4759  xpiundir  4760  cnvuni  4882  dmiun  4903  elres  5006  elsnres  5007  rniun  5107  imaco  5194  coiun  5198  fun11iun  5509  abrexco  5782  imaiun  5787  fliftf  5830  oprabrexex2  5979  releldm2  6186  oarec  6576  omeu  6599  eroveu  6769  dfac5lem2  7767  genpass  8649  supmul1  9735  supmullem2  9737  supmul  9738  pceu  12915  4sqlem12  13019  mreiincl  13514  ntreq0  16830  metrest  18086  nofulllem5  24431  elfuns  24525  supaddc  24995  supadd  24996  itg2addnc  25005  sdclem1  26556  prter2  26852  diophrex  26958  psgneu  27532  bnj906  29278  lshpsmreu  29921  islpln5  30346  islvol5  30390  cdlemftr3  31376  mapdpglem3  32487  hdmapglem7a  32742
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803
  Copyright terms: Public domain W3C validator