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

Theorem rexcom4 3133
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 3023 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 3128 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2965 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 3128 . 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 1596   E.wrex 2815   _Vcvv 3113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-v 3115
This theorem is referenced by:  rexcom4a  3134  reuind  3307  uni0b  4270  iuncom4  4333  dfiun2g  4357  iunn0  4385  iunxiun  4408  iinexg  4607  inuni  4609  iunopab  4783  xpiundi  5054  xpiundir  5055  cnvuni  5189  dmiun  5211  elres  5309  elsnres  5310  rniun  5416  xpdifid  5435  imaco  5512  coiun  5517  abrexco  6144  imaiun  6145  fliftf  6201  fun11iun  6744  oprabrexex2  6774  releldm2  6834  oarec  7211  omeu  7234  eroveu  7406  dfac5lem2  8505  genpass  9387  supmul1  10508  supmullem2  10510  supmul  10511  pceu  14229  4sqlem12  14333  mreiincl  14851  psgneu  16337  ntreq0  19372  metrest  20790  metuel2  20845  istrkg2ld  23614  el2wlkonot  24573  el2spthonot  24574  el2wlkonotot0  24576  fpwrelmapffslem  27255  nofulllem5  29071  supaddc  29646  supadd  29647  ismblfin  29660  itg2addnclem3  29673  sdclem1  29867  prter2  30254  diophrex  30341  upbdrech  31110  bnj906  33085  bj-elsngl  33625  lshpsmreu  33924  islpln5  34349  islvol5  34393  cdlemftr3  35379  mapdpglem3  36490  hdmapglem7a  36745
  Copyright terms: Public domain W3C validator