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

Theorem rexcom4 3067
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 2952 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 3062 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2889 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 3062 . 2  |-  ( E. y  e.  _V  E. x  e.  A  ph  <->  E. y E. x  e.  A  ph )
51, 3, 43bitr3i 279 1  |-  ( E. x  e.  A  E. y ph  <->  E. y E. x  e.  A  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188   E.wex 1663   E.wrex 2738   _Vcvv 3045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-v 3047
This theorem is referenced by:  rexcom4a  3068  reuind  3243  uni0b  4223  iuncom4  4286  dfiun2g  4310  iunn0  4338  iunxiun  4364  iinexg  4563  inuni  4565  iunopab  4737  xpiundi  4889  xpiundir  4890  cnvuni  5021  dmiun  5043  elres  5140  elsnres  5141  rniun  5246  xpdifid  5265  imaco  5340  coiun  5345  abrexco  6149  imaiun  6150  fliftf  6208  fun11iun  6753  oprabrexex2  6783  releldm2  6843  oarec  7263  omeu  7286  eroveu  7458  dfac5lem2  8555  genpass  9434  supaddc  10574  supadd  10575  supmul1  10576  supmullem2  10578  supmul  10579  pceu  14796  4sqlem12  14900  mreiincl  15502  psgneu  17147  ntreq0  20093  unisngl  20542  metrest  21539  metuel2  21580  istrkg2ld  24508  el2wlkonot  25597  el2spthonot  25598  el2wlkonotot0  25600  fpwrelmapffslem  28317  omssubaddlem  29127  omssubadd  29128  omssubaddlemOLD  29131  omssubaddOLD  29132  bnj906  29741  nofulllem5  30595  bj-elsngl  31562  ismblfin  31981  itg2addnclem3  31995  sdclem1  32072  prter2  32453  lshpsmreu  32675  islpln5  33100  islvol5  33144  cdlemftr3  34132  mapdpglem3  35243  hdmapglem7a  35498  diophrex  35618  imaiun1  36243  coiun1  36244  upbdrech  37523
  Copyright terms: Public domain W3C validator