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

Theorem eluni2 4011
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 1596 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4010 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2703 . 2  |-  ( E. x  e.  B  A  e.  x  <->  E. x ( x  e.  B  /\  A  e.  x ) )
41, 2, 33bitr4i 269 1  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1550    e. wcel 1725   E.wrex 2698   U.cuni 4007
This theorem is referenced by:  uni0b  4032  intssuni  4064  iuncom4  4092  inuni  4354  ssorduni  4758  unon  4803  limuni3  4824  cnvuni  5049  chfnrn  5833  onfununi  6595  oarec  6797  uniinqs  6976  fissuni  7403  finsschain  7405  r1sdom  7692  rankuni2b  7771  cflm  8122  coflim  8133  axdc3lem2  8323  fpwwe2lem12  8508  uniwun  8607  tskr1om2  8635  tskuni  8650  axgroth3  8698  inaprc  8703  tskmval  8706  tskmcl  8708  suplem1pr  8921  lbsextlem2  16223  lbsextlem3  16224  isbasis3g  17006  eltg2b  17016  unitg  17024  tgcl  17026  ppttop  17063  epttop  17065  neiptoptop  17187  tgcmp  17456  1stckgenlem  17577  txuni2  17589  txcmplem1  17665  tgqtop  17736  filuni  17909  alexsubALTlem4  18073  ptcmplem3  18077  ptcmplem4  18078  utoptop  18256  icccmplem1  18845  icccmplem3  18847  cnheibor  18972  bndth  18975  lebnumlem1  18978  bcthlem4  19272  ovolicc2lem5  19409  dyadmbllem  19483  itg2gt0  19644  rexunirn  23970  unipreima  24048  dya2iocuni  24625  cvmsss2  24953  cvmseu  24955  untuni  25150  dfon2lem3  25404  dfon2lem7  25408  dfon2lem8  25409  brbigcup  25735  mblfinlem  26234  locfincmp  26375  comppfsc  26378  neibastop1  26379  neibastop2lem  26380  cover2  26406  heiborlem9  26519  unichnidl  26632  prtlem16  26709  prter2  26721  prter3  26722  bnj1379  29139
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-v 2950  df-uni 4008
  Copyright terms: Public domain W3C validator