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

Theorem eliun 4099
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 2966 . 2  |-  ( A  e.  U_ x  e.  B  C  ->  A  e.  _V )
2 elex 2966 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32rexlimivw 2828 . 2  |-  ( E. x  e.  B  A  e.  C  ->  A  e. 
_V )
4 eleq1 2498 . . . 4  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
54rexbidv 2728 . . 3  |-  ( y  =  A  ->  ( E. x  e.  B  y  e.  C  <->  E. x  e.  B  A  e.  C ) )
6 df-iun 4097 . . 3  |-  U_ x  e.  B  C  =  { y  |  E. x  e.  B  y  e.  C }
75, 6elab2g 3086 . 2  |-  ( A  e.  _V  ->  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C ) )
81, 3, 7pm5.21nii 344 1  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653    e. wcel 1726   E.wrex 2708   _Vcvv 2958   U_ciun 4095
This theorem is referenced by:  iuncom  4101  iuncom4  4102  iunconst  4103  iuniin  4105  iunss1  4106  ss2iun  4110  dfiun2g  4125  ssiun  4135  ssiun2  4136  iunab  4139  iun0  4149  0iun  4150  iunn0  4153  iunin2  4157  iundif2  4160  iindif2  4162  iunxsng  4171  iunun  4173  iunxun  4174  iunxiun  4175  iunpwss  4182  disjiun  4204  disjxiun  4211  triun  4317  iunpw  4761  xpiundi  4934  xpiundir  4935  iunxpf  5023  cnvuni  5059  dmiun  5080  dmuni  5081  rniun  5284  dfco2  5371  dfco2a  5372  coiun  5381  fun11iun  5697  opabex3d  5991  opabex3  5992  imaiun  5994  eluniima  5999  onoviun  6607  smoiun  6625  oalimcl  6805  oaass  6806  oarec  6807  omordlim  6822  omlimcl  6823  omeulem1  6827  oeordi  6832  oelimcl  6845  oeeulem  6846  oaabs2  6890  omabs  6892  dffi3  7438  ixpiunwdom  7561  trcl  7666  r1ordg  7706  r1pwss  7712  rankr1ai  7726  r1elss  7734  fseqenlem2  7908  fseqdom  7909  infpwfien  7945  cardaleph  7972  ackbij2  8125  cfsmolem  8152  alephsing  8158  hsmexlem2  8309  axdc3lem2  8333  ac6c4  8363  ttukeylem6  8396  iunfo  8416  iundom2g  8417  konigthlem  8445  alephreg  8459  pwcfsdom  8460  pwfseqlem3  8537  inar1  8652  inatsk  8655  wrdval  11732  fsum2dlem  12556  fsumcom2  12560  fsumiun  12602  prmreclem5  13290  imasaddfnlem  13755  imasvscafn  13764  efgs1b  15370  efgsfo  15373  frgpnabllem1  15486  lssats2  16078  lbsextlem2  16233  lbsextlem3  16234  islpidl  16319  iunocv  16910  iunconlem  17492  iuncon  17493  alexsubALTlem3  18082  ptcmplem3  18087  imasdsf1olem  18405  zcld  18846  ovolfioo  19366  ovolficc  19367  ovoliunlem2  19401  ovoliunnul  19405  volfiniun  19443  iundisj  19444  iunmbl2  19453  volsup2  19499  vitalilem2  19503  ismbf3d  19548  mbfaddlem  19554  mbfsup  19558  i1faddlem  19587  i1fmullem  19588  elaa  20235  ssiun3  24011  iundisjf  24031  unipreima  24058  ofpreima  24083  iundisjfi  24154  dstfrvunirn  24734  dfrtrclrec2  25145  fprod2dlem  25306  fprodcom2  25310  eltrpred  25506  dftrpred3g  25513  trpredrec  25518  wfrlem9  25548  frrlem5e  25592  nofulllem5  25663  colinearex  25996  rabiun  26238  volsupnfl  26253  locfincmp  26386  neibastop2lem  26391  istotbnd3  26482  sstotbnd  26486  sstotbnd3  26487  prdstotbnd  26505  cntotbnd  26507  heiborlem3  26524  heibor  26532  otiunsndisj  28069  otiunsndisjX  28070  2spotiundisj  28513  usgreg2spot  28518  iunconlem2  29109  bnj1405  29270  bnj916  29366  bnj983  29384  bnj1398  29465  bnj1417  29472  bnj1498  29492  pclfinN  30759  pclcmpatN  30760  lcfrvalsnN  32401  lcfrlem5  32406  lcfrlem6  32407  lcfrlem16  32418  lcfrlem27  32429  lcfrlem37  32439  lcfr  32445  mapdrvallem2  32505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-iun 4097
  Copyright terms: Public domain W3C validator