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

Theorem eluni2 4095
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 1638 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4094 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2721 . 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 1586    e. wcel 1756   E.wrex 2716   U.cuni 4091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-v 2974  df-uni 4092
This theorem is referenced by:  uni0b  4116  intssuni  4150  iuncom4  4178  inuni  4454  cnvuni  5026  chfnrn  5814  ssorduni  6397  unon  6442  limuni3  6463  onfununi  6802  oarec  7001  uniinqs  7180  fissuni  7616  finsschain  7618  r1sdom  7981  rankuni2b  8060  cflm  8419  coflim  8430  axdc3lem2  8620  fpwwe2lem12  8808  uniwun  8907  tskr1om2  8935  tskuni  8950  axgroth3  8998  inaprc  9003  tskmval  9006  tskmcl  9008  suplem1pr  9221  lbsextlem2  17240  lbsextlem3  17241  isbasis3g  18554  eltg2b  18564  unitg  18572  tgcl  18574  ppttop  18611  epttop  18613  neiptoptop  18735  tgcmp  19004  1stckgenlem  19126  txuni2  19138  txcmplem1  19214  tgqtop  19285  filuni  19458  alexsubALTlem4  19622  ptcmplem3  19626  ptcmplem4  19627  utoptop  19809  icccmplem1  20399  icccmplem3  20401  cnheibor  20527  bndth  20530  lebnumlem1  20533  bcthlem4  20838  ovolicc2lem5  21004  dyadmbllem  21079  itg2gt0  21238  rexunirn  25875  unipreima  25961  ddemeas  26652  dya2iocuni  26698  cvmsss2  27163  cvmseu  27165  untuni  27360  dfon2lem3  27598  dfon2lem7  27602  dfon2lem8  27603  brbigcup  27929  heicant  28426  mblfinlem1  28428  locfincmp  28576  comppfsc  28579  neibastop1  28580  neibastop2lem  28581  cover2  28607  heiborlem9  28718  unichnidl  28831  prtlem16  29014  prter2  29026  prter3  29027  bnj1379  31824
  Copyright terms: Public domain W3C validator