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

Theorem eluni2 4216
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 1733 . 2  |-  ( E. x ( A  e.  x  /\  x  e.  B )  <->  E. x
( x  e.  B  /\  A  e.  x
) )
2 eluni 4215 . 2  |-  ( A  e.  U. B  <->  E. x
( A  e.  x  /\  x  e.  B
) )
3 df-rex 2755 . 2  |-  ( E. x  e.  B  A  e.  x  <->  E. x ( x  e.  B  /\  A  e.  x ) )
41, 2, 33bitr4i 285 1  |-  ( A  e.  U. B  <->  E. x  e.  B  A  e.  x )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375   E.wex 1674    e. wcel 1898   E.wrex 2750   U.cuni 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rex 2755  df-v 3059  df-uni 4213
This theorem is referenced by:  uni0b  4237  intssuni  4271  iuncom4  4300  inuni  4582  cnvuni  5043  chfnrn  6021  ssorduni  6644  unon  6690  limuni3  6711  onfununi  7091  oarec  7294  uniinqs  7474  fissuni  7910  finsschain  7912  r1sdom  8276  rankuni2b  8355  cflm  8711  coflim  8722  axdc3lem2  8912  fpwwe2lem12  9097  uniwun  9196  tskr1om2  9224  tskuni  9239  axgroth3  9287  inaprc  9292  tskmval  9295  tskmcl  9297  suplem1pr  9508  lbsextlem2  18437  lbsextlem3  18438  isbasis3g  20019  eltg2b  20029  unitgOLD  20038  tgcl  20040  ppttop  20077  epttop  20079  neiptoptop  20202  tgcmp  20471  locfincmp  20596  dissnref  20598  comppfsc  20602  1stckgenlem  20623  txuni2  20635  txcmplem1  20711  tgqtop  20782  filuni  20955  alexsubALTlem4  21120  ptcmplem3  21124  ptcmplem4  21125  utoptop  21304  icccmplem1  21895  icccmplem3  21897  cnheibor  22038  bndth  22041  lebnumlem1  22044  lebnumlem1OLD  22047  bcthlem4  22350  ovolicc2lem5  22530  dyadmbllem  22613  itg2gt0  22774  rexunirn  28183  unipreima  28298  acunirnmpt2  28314  acunirnmpt2f  28315  reff  28717  locfinreflem  28718  cmpcref  28728  ddemeas  29109  dya2iocuni  29155  bnj1379  29692  cvmsss2  30047  cvmseu  30049  untuni  30386  dfon2lem3  30481  dfon2lem7  30485  dfon2lem8  30486  brbigcup  30715  neibastop1  31065  neibastop2lem  31066  heicant  32021  mblfinlem1  32023  cover2  32086  heiborlem9  32197  unichnidl  32310  prtlem16  32487  prter2  32499  prter3  32500  disjinfi  37522  cncfuni  37850  intsaluni  38289  salgencntex  38303
  Copyright terms: Public domain W3C validator