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

Theorem eliun 3909
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 2796 . 2  |-  ( A  e.  U_ x  e.  B  C  ->  A  e.  _V )
2 elex 2796 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32rexlimivw 2663 . 2  |-  ( E. x  e.  B  A  e.  C  ->  A  e. 
_V )
4 eleq1 2343 . . . 4  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
54rexbidv 2564 . . 3  |-  ( y  =  A  ->  ( E. x  e.  B  y  e.  C  <->  E. x  e.  B  A  e.  C ) )
6 df-iun 3907 . . 3  |-  U_ x  e.  B  C  =  { y  |  E. x  e.  B  y  e.  C }
75, 6elab2g 2916 . 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 1623    e. wcel 1684   E.wrex 2544   _Vcvv 2788   U_ciun 3905
This theorem is referenced by:  iuncom  3911  iuncom4  3912  iunconst  3913  iuniin  3915  iunss1  3916  ss2iun  3920  dfiun2g  3935  ssiun  3944  ssiun2  3945  iunab  3948  iun0  3958  0iun  3959  iunn0  3962  iunin2  3966  iundif2  3969  iindif2  3971  iunxsng  3980  iunun  3982  iunxun  3983  iunxiun  3984  iunpwss  3991  disjiun  4013  disjxiun  4020  triun  4126  iunpw  4570  xpiundi  4743  xpiundir  4744  iunxpf  4832  cnvuni  4866  dmiun  4887  dmuni  4888  rniun  5091  dfco2  5172  dfco2a  5173  coiun  5182  fun11iun  5493  opabex3  5769  imaiun  5771  eluniima  5776  onoviun  6360  smoiun  6378  oalimcl  6558  oaass  6559  oarec  6560  omordlim  6575  omlimcl  6576  omeulem1  6580  oeordi  6585  oelimcl  6598  oeeulem  6599  oaabs2  6643  omabs  6645  dffi3  7184  ixpiunwdom  7305  trcl  7410  r1ordg  7450  r1pwss  7456  rankr1ai  7470  r1elss  7478  fseqenlem2  7652  fseqdom  7653  infpwfien  7689  cardaleph  7716  ackbij2  7869  cfsmolem  7896  alephsing  7902  hsmexlem2  8053  axdc3lem2  8077  ac6c4  8108  ttukeylem6  8141  iunfo  8161  iundom2g  8162  konigthlem  8190  alephreg  8204  pwcfsdom  8205  pwfseqlem3  8282  inar1  8397  inatsk  8400  wrdval  11416  fsum2dlem  12233  fsumcom2  12237  fsumiun  12279  prmreclem5  12967  imasaddfnlem  13430  imasvscafn  13439  efgs1b  15045  efgsfo  15048  frgpnabllem1  15161  lssats2  15757  lbsextlem2  15912  lbsextlem3  15913  islpidl  15998  iunocv  16581  iunconlem  17153  iuncon  17154  alexsubALTlem3  17743  ptcmplem3  17748  imasdsf1olem  17937  zcld  18319  ovolfioo  18827  ovolficc  18828  ovoliunlem2  18862  ovoliunnul  18866  volfiniun  18904  iundisj  18905  iunmbl2  18914  volsup2  18960  vitalilem2  18964  ismbf3d  19009  mbfaddlem  19015  mbfsup  19019  i1faddlem  19048  i1fmullem  19049  elaa  19696  unipreima  23209  iundisjfi  23363  iundisjf  23365  dstfrvunirn  23675  dfrtrclrec2  24040  eltrpred  24229  dftrpred3g  24236  trpredrec  24241  wfrlem9  24264  frrlem5e  24289  nofulllem5  24360  colinearex  24683  eqfnung2  25118  dstr  25171  iscst4  25177  nsn  25530  osneisi  25531  prismorcsetlem  25912  prismorcset  25914  1iskle  25989  empklst  26009  clscnc  26010  phckle  26027  psckle  26028  locfincmp  26304  neibastop2lem  26309  istotbnd3  26495  sstotbnd  26499  sstotbnd3  26500  prdstotbnd  26518  cntotbnd  26520  heiborlem3  26537  heibor  26545  bnj1405  28869  bnj916  28965  bnj983  28983  bnj1398  29064  bnj1417  29071  bnj1498  29091  pclfinN  30089  pclcmpatN  30090  lcfrvalsnN  31731  lcfrlem5  31736  lcfrlem6  31737  lcfrlem16  31748  lcfrlem27  31759  lcfrlem37  31769  lcfr  31775  mapdrvallem2  31835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-v 2790  df-iun 3907
  Copyright terms: Public domain W3C validator