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

Theorem eluni2 4253
Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
eluni2
Distinct variable groups:   ,   ,

Proof of Theorem eluni2
StepHypRef Expression
1 exancom 1671 . 2
2 eluni 4252 . 2
3 df-rex 2813 . 2
41, 2, 33bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  E.wex 1612  e.wcel 1818  E.wrex 2808  U.cuni 4249
This theorem is referenced by:  uni0b  4274  intssuni  4309  iuncom4  4338  inuni  4614  cnvuni  5194  chfnrn  5998  ssorduni  6621  unon  6666  limuni3  6687  onfununi  7031  oarec  7230  uniinqs  7410  fissuni  7845  finsschain  7847  r1sdom  8213  rankuni2b  8292  cflm  8651  coflim  8662  axdc3lem2  8852  fpwwe2lem12  9040  uniwun  9139  tskr1om2  9167  tskuni  9182  axgroth3  9230  inaprc  9235  tskmval  9238  tskmcl  9240  suplem1pr  9451  lbsextlem2  17805  lbsextlem3  17806  isbasis3g  19450  eltg2b  19460  unitgOLD  19469  tgcl  19471  ppttop  19508  epttop  19510  neiptoptop  19632  tgcmp  19901  locfincmp  20027  dissnref  20029  comppfsc  20033  1stckgenlem  20054  txuni2  20066  txcmplem1  20142  tgqtop  20213  filuni  20386  alexsubALTlem4  20550  ptcmplem3  20554  ptcmplem4  20555  utoptop  20737  icccmplem1  21327  icccmplem3  21329  cnheibor  21455  bndth  21458  lebnumlem1  21461  bcthlem4  21766  ovolicc2lem5  21932  dyadmbllem  22008  itg2gt0  22167  rexunirn  27390  unipreima  27484  reff  27842  locfinreflem  27843  cmpcref  27853  ddemeas  28208  dya2iocuni  28254  cvmsss2  28719  cvmseu  28721  untuni  29081  dfon2lem3  29217  dfon2lem7  29221  dfon2lem8  29222  brbigcup  29548  heicant  30049  mblfinlem1  30051  neibastop1  30177  neibastop2lem  30178  cover2  30204  heiborlem9  30315  unichnidl  30428  prtlem16  30610  prter2  30622  prter3  30623  cncfuni  31689  bnj1379  33889
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-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-rex 2813  df-v 3111  df-uni 4250
  Copyright terms: Public domain W3C validator