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

Theorem eluni2 3962
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 1593 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 3961 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2656 . 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 1547    e. wcel 1717   E.wrex 2651   U.cuni 3958
This theorem is referenced by:  uni0b  3983  intssuni  4015  iuncom4  4043  inuni  4304  ssorduni  4707  unon  4752  limuni3  4773  cnvuni  4998  chfnrn  5781  onfununi  6540  oarec  6742  uniinqs  6921  fissuni  7347  finsschain  7349  r1sdom  7634  rankuni2b  7713  cflm  8064  coflim  8075  axdc3lem2  8265  fpwwe2lem12  8450  uniwun  8549  tskr1om2  8577  tskuni  8592  axgroth3  8640  inaprc  8645  tskmval  8648  tskmcl  8650  suplem1pr  8863  lbsextlem2  16159  lbsextlem3  16160  isbasis3g  16938  eltg2b  16948  unitg  16956  tgcl  16958  ppttop  16995  epttop  16997  neiptoptop  17119  tgcmp  17387  1stckgenlem  17507  txuni2  17519  txcmplem1  17595  tgqtop  17666  filuni  17839  alexsubALTlem4  18003  ptcmplem3  18007  ptcmplem4  18008  utoptop  18186  icccmplem1  18725  icccmplem3  18727  cnheibor  18852  bndth  18855  lebnumlem1  18858  bcthlem4  19150  ovolicc2lem5  19285  dyadmbllem  19359  itg2gt0  19520  rexunirn  23823  unipreima  23899  dya2iocuni  24428  cvmsss2  24741  cvmseu  24743  untuni  24938  dfon2lem3  25166  dfon2lem7  25170  dfon2lem8  25171  brbigcup  25463  locfincmp  26076  comppfsc  26079  neibastop1  26080  neibastop2lem  26081  cover2  26107  heiborlem9  26220  unichnidl  26333  prtlem16  26410  prter2  26422  prter3  26423  bnj1379  28541
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-rex 2656  df-v 2902  df-uni 3959
  Copyright terms: Public domain W3C validator