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

Theorem rexcom4 3115
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 3005 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. y  e.  _V  E. x  e.  A  ph )
2 rexv 3110 . . 3  |-  ( E. y  e.  _V  ph  <->  E. y ph )
32rexbii 2945 . 2  |-  ( E. x  e.  A  E. y  e.  _V  ph  <->  E. x  e.  A  E. y ph )
4 rexv 3110 . 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 1599   E.wrex 2794   _Vcvv 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-v 3097
This theorem is referenced by:  rexcom4a  3116  reuind  3289  uni0b  4259  iuncom4  4323  dfiun2g  4347  iunn0  4375  iunxiun  4398  iinexg  4597  inuni  4599  iunopab  4773  xpiundi  5044  xpiundir  5045  cnvuni  5179  dmiun  5201  elres  5299  elsnres  5300  rniun  5406  xpdifid  5425  imaco  5502  coiun  5507  abrexco  6141  imaiun  6142  fliftf  6198  fun11iun  6745  oprabrexex2  6775  releldm2  6835  oarec  7213  omeu  7236  eroveu  7408  dfac5lem2  8508  genpass  9390  supmul1  10515  supmullem2  10517  supmul  10518  pceu  14352  4sqlem12  14456  mreiincl  14975  psgneu  16510  ntreq0  19556  unisngl  20006  metrest  21005  metuel2  21060  istrkg2ld  23836  el2wlkonot  24847  el2spthonot  24848  el2wlkonotot0  24850  fpwrelmapffslem  27533  nofulllem5  29442  supaddc  30017  supadd  30018  ismblfin  30031  itg2addnclem3  30044  sdclem1  30212  prter2  30598  diophrex  30685  upbdrech  31459  bnj906  33856  bj-elsngl  34409  lshpsmreu  34709  islpln5  35134  islvol5  35178  cdlemftr3  36166  mapdpglem3  37277  hdmapglem7a  37532
  Copyright terms: Public domain W3C validator