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

Theorem eliun 3925
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)

Proof of Theorem eliun
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 elex 2809 . 2  |-  ( A  e.  U_ x  e.  B  C  ->  A  e.  _V )
2 elex 2809 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32rexlimivw 2676 . 2  |-  ( E. x  e.  B  A  e.  C  ->  A  e. 
_V )
4 eleq1 2356 . . . 4  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
54rexbidv 2577 . . 3  |-  ( y  =  A  ->  ( E. x  e.  B  y  e.  C  <->  E. x  e.  B  A  e.  C ) )
6 df-iun 3923 . . 3  |-  U_ x  e.  B  C  =  { y  |  E. x  e.  B  y  e.  C }
75, 6elab2g 2929 . 2  |-  ( A  e.  _V  ->  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C ) )
81, 3, 7pm5.21nii 342 1  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    e. wcel 1696   E.wrex 2557   _Vcvv 2801   U_ciun 3921
This theorem is referenced by:  iuncom  3927  iuncom4  3928  iunconst  3929  iuniin  3931  iunss1  3932  ss2iun  3936  dfiun2g  3951  ssiun  3960  ssiun2  3961  iunab  3964  iun0  3974  0iun  3975  iunn0  3978  iunin2  3982  iundif2  3985  iindif2  3987  iunxsng  3996  iunun  3998  iunxun  3999  iunxiun  4000  iunpwss  4007  disjiun  4029  disjxiun  4036  triun  4142  iunpw  4586  xpiundi  4759  xpiundir  4760  iunxpf  4848  cnvuni  4882  dmiun  4903  dmuni  4904  rniun  5107  dfco2  5188  dfco2a  5189  coiun  5198  fun11iun  5509  opabex3  5785  imaiun  5787  eluniima  5792  onoviun  6376  smoiun  6394  oalimcl  6574  oaass  6575  oarec  6576  omordlim  6591  omlimcl  6592  omeulem1  6596  oeordi  6601  oelimcl  6614  oeeulem  6615  oaabs2  6659  omabs  6661  dffi3  7200  ixpiunwdom  7321  trcl  7426  r1ordg  7466  r1pwss  7472  rankr1ai  7486  r1elss  7494  fseqenlem2  7668  fseqdom  7669  infpwfien  7705  cardaleph  7732  ackbij2  7885  cfsmolem  7912  alephsing  7918  hsmexlem2  8069  axdc3lem2  8093  ac6c4  8124  ttukeylem6  8157  iunfo  8177  iundom2g  8178  konigthlem  8206  alephreg  8220  pwcfsdom  8221  pwfseqlem3  8298  inar1  8413  inatsk  8416  wrdval  11432  fsum2dlem  12249  fsumcom2  12253  fsumiun  12295  prmreclem5  12983  imasaddfnlem  13446  imasvscafn  13455  efgs1b  15061  efgsfo  15064  frgpnabllem1  15177  lssats2  15773  lbsextlem2  15928  lbsextlem3  15929  islpidl  16014  iunocv  16597  iunconlem  17169  iuncon  17170  alexsubALTlem3  17759  ptcmplem3  17764  imasdsf1olem  17953  zcld  18335  ovolfioo  18843  ovolficc  18844  ovoliunlem2  18878  ovoliunnul  18882  volfiniun  18920  iundisj  18921  iunmbl2  18930  volsup2  18976  vitalilem2  18980  ismbf3d  19025  mbfaddlem  19031  mbfsup  19035  i1faddlem  19064  i1fmullem  19065  elaa  19712  unipreima  23224  iundisjfi  23378  iundisjf  23380  dstfrvunirn  23690  dfrtrclrec2  24055  eltrpred  24300  dftrpred3g  24307  trpredrec  24312  wfrlem9  24335  frrlem5e  24360  nofulllem5  24431  colinearex  24755  rabiun2  24997  eqfnung2  25221  dstr  25274  iscst4  25280  nsn  25633  osneisi  25634  prismorcsetlem  26015  prismorcset  26017  1iskle  26092  empklst  26112  clscnc  26113  phckle  26130  psckle  26131  locfincmp  26407  neibastop2lem  26412  istotbnd3  26598  sstotbnd  26602  sstotbnd3  26603  prdstotbnd  26621  cntotbnd  26623  heiborlem3  26640  heibor  26648  opabex3d  28190  bnj1405  29185  bnj916  29281  bnj983  29299  bnj1398  29380  bnj1417  29387  bnj1498  29407  pclfinN  30711  pclcmpatN  30712  lcfrvalsnN  32353  lcfrlem5  32358  lcfrlem6  32359  lcfrlem16  32370  lcfrlem27  32381  lcfrlem37  32391  lcfr  32397  mapdrvallem2  32457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-v 2803  df-iun 3923
  Copyright terms: Public domain W3C validator