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

Theorem rexcom4 3129
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
Distinct variable groups:   ,   ,

Proof of Theorem rexcom4
StepHypRef Expression
1 rexcom 3019 . 2
2 rexv 3124 . . 3
32rexbii 2959 . 2
4 rexv 3124 . 2
51, 3, 43bitr3i 275 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612  E.wrex 2808   cvv 3109
This theorem is referenced by:  rexcom4a  3130  reuind  3303  uni0b  4274  iuncom4  4338  dfiun2g  4362  iunn0  4390  iunxiun  4413  iinexg  4612  inuni  4614  iunopab  4788  xpiundi  5059  xpiundir  5060  cnvuni  5194  dmiun  5216  elres  5314  elsnres  5315  rniun  5421  xpdifid  5440  imaco  5517  coiun  5522  abrexco  6156  imaiun  6157  fliftf  6213  fun11iun  6760  oprabrexex2  6790  releldm2  6850  oarec  7230  omeu  7253  eroveu  7425  dfac5lem2  8526  genpass  9408  supmul1  10533  supmullem2  10535  supmul  10536  pceu  14370  4sqlem12  14474  mreiincl  14993  psgneu  16531  ntreq0  19578  unisngl  20028  metrest  21027  metuel2  21082  istrkg2ld  23858  el2wlkonot  24869  el2spthonot  24870  el2wlkonotot0  24872  fpwrelmapffslem  27555  nofulllem5  29466  supaddc  30041  supadd  30042  ismblfin  30055  itg2addnclem3  30068  sdclem1  30236  prter2  30622  diophrex  30709  upbdrech  31505  bnj906  33988  bj-elsngl  34526  lshpsmreu  34834  islpln5  35259  islvol5  35303  cdlemftr3  36291  mapdpglem3  37402  hdmapglem7a  37657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111
  Copyright terms: Public domain W3C validator