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

Theorem eluni2 4255
Description: Membership in class union. Restricted quantifier version. (Contributed by NM, 31-Aug-1999.)
Assertion
Ref Expression
eluni2  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Distinct variable groups:    x, A    x, B

Proof of Theorem eluni2
StepHypRef Expression
1 exancom 1672 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4254 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2813 . 2  |-  ( E. x  e.  B  A  e.  x  <->  E. x ( x  e.  B  /\  A  e.  x ) )
41, 2, 33bitr4i 277 1  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   E.wex 1613    e. wcel 1819   E.wrex 2808   U.cuni 4251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-uni 4252
This theorem is referenced by:  uni0b  4276  intssuni  4311  iuncom4  4340  inuni  4618  cnvuni  5199  chfnrn  5999  ssorduni  6620  unon  6665  limuni3  6686  onfununi  7030  oarec  7229  uniinqs  7409  fissuni  7843  finsschain  7845  r1sdom  8209  rankuni2b  8288  cflm  8647  coflim  8658  axdc3lem2  8848  fpwwe2lem12  9036  uniwun  9135  tskr1om2  9163  tskuni  9178  axgroth3  9226  inaprc  9231  tskmval  9234  tskmcl  9236  suplem1pr  9447  lbsextlem2  17932  lbsextlem3  17933  isbasis3g  19577  eltg2b  19587  unitgOLD  19596  tgcl  19598  ppttop  19635  epttop  19637  neiptoptop  19759  tgcmp  20028  locfincmp  20153  dissnref  20155  comppfsc  20159  1stckgenlem  20180  txuni2  20192  txcmplem1  20268  tgqtop  20339  filuni  20512  alexsubALTlem4  20676  ptcmplem3  20680  ptcmplem4  20681  utoptop  20863  icccmplem1  21453  icccmplem3  21455  cnheibor  21581  bndth  21584  lebnumlem1  21587  bcthlem4  21892  ovolicc2lem5  22058  dyadmbllem  22134  itg2gt0  22293  rexunirn  27517  unipreima  27632  acunirnmpt2  27654  acunirnmpt2f  27655  reff  28003  locfinreflem  28004  cmpcref  28014  ddemeas  28381  dya2iocuni  28427  cvmsss2  28916  cvmseu  28918  untuni  29278  dfon2lem3  29413  dfon2lem7  29417  dfon2lem8  29418  brbigcup  29732  heicant  30233  mblfinlem1  30235  neibastop1  30361  neibastop2lem  30362  cover2  30388  heiborlem9  30499  unichnidl  30612  prtlem16  30794  prter2  30806  prter3  30807  cncfuni  31871  bnj1379  34011
  Copyright terms: Public domain W3C validator