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

Theorem eluni2 4249
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 1648 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4248 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2820 . 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 1596    e. wcel 1767   E.wrex 2815   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-v 3115  df-uni 4246
This theorem is referenced by:  uni0b  4270  intssuni  4304  iuncom4  4333  inuni  4609  cnvuni  5188  chfnrn  5991  ssorduni  6600  unon  6645  limuni3  6666  onfununi  7012  oarec  7211  uniinqs  7391  fissuni  7824  finsschain  7826  r1sdom  8191  rankuni2b  8270  cflm  8629  coflim  8640  axdc3lem2  8830  fpwwe2lem12  9018  uniwun  9117  tskr1om2  9145  tskuni  9160  axgroth3  9208  inaprc  9213  tskmval  9216  tskmcl  9218  suplem1pr  9429  lbsextlem2  17600  lbsextlem3  17601  isbasis3g  19233  eltg2b  19243  unitg  19251  tgcl  19253  ppttop  19290  epttop  19292  neiptoptop  19414  tgcmp  19683  1stckgenlem  19805  txuni2  19817  txcmplem1  19893  tgqtop  19964  filuni  20137  alexsubALTlem4  20301  ptcmplem3  20305  ptcmplem4  20306  utoptop  20488  icccmplem1  21078  icccmplem3  21080  cnheibor  21206  bndth  21209  lebnumlem1  21212  bcthlem4  21517  ovolicc2lem5  21683  dyadmbllem  21759  itg2gt0  21918  rexunirn  27082  unipreima  27172  ddemeas  27864  dya2iocuni  27910  cvmsss2  28375  cvmseu  28377  untuni  28572  dfon2lem3  28810  dfon2lem7  28814  dfon2lem8  28815  brbigcup  29141  heicant  29642  mblfinlem1  29644  locfincmp  29792  comppfsc  29795  neibastop1  29796  neibastop2lem  29797  cover2  29823  heiborlem9  29934  unichnidl  30047  prtlem16  30230  prter2  30242  prter3  30243  cncfuni  31241  bnj1379  32977
  Copyright terms: Public domain W3C validator