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

Theorem eluni2 3979
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 3978 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2672 . 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 1721   E.wrex 2667   U.cuni 3975
This theorem is referenced by:  uni0b  4000  intssuni  4032  iuncom4  4060  inuni  4322  ssorduni  4725  unon  4770  limuni3  4791  cnvuni  5016  chfnrn  5800  onfununi  6562  oarec  6764  uniinqs  6943  fissuni  7369  finsschain  7371  r1sdom  7656  rankuni2b  7735  cflm  8086  coflim  8097  axdc3lem2  8287  fpwwe2lem12  8472  uniwun  8571  tskr1om2  8599  tskuni  8614  axgroth3  8662  inaprc  8667  tskmval  8670  tskmcl  8672  suplem1pr  8885  lbsextlem2  16186  lbsextlem3  16187  isbasis3g  16969  eltg2b  16979  unitg  16987  tgcl  16989  ppttop  17026  epttop  17028  neiptoptop  17150  tgcmp  17418  1stckgenlem  17538  txuni2  17550  txcmplem1  17626  tgqtop  17697  filuni  17870  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem4  18039  utoptop  18217  icccmplem1  18806  icccmplem3  18808  cnheibor  18933  bndth  18936  lebnumlem1  18939  bcthlem4  19233  ovolicc2lem5  19370  dyadmbllem  19444  itg2gt0  19605  rexunirn  23931  unipreima  24009  dya2iocuni  24586  cvmsss2  24914  cvmseu  24916  untuni  25111  dfon2lem3  25355  dfon2lem7  25359  dfon2lem8  25360  brbigcup  25652  mblfinlem  26143  locfincmp  26274  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  cover2  26305  heiborlem9  26418  unichnidl  26531  prtlem16  26608  prter2  26620  prter3  26621  bnj1379  28908
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-v 2918  df-uni 3976
  Copyright terms: Public domain W3C validator