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

Theorem eliun 4335
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun
Distinct variable group:   ,

Proof of Theorem eliun
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . 3
32rexlimivw 2946 . 2
4 eleq1 2529 . . . 4
54rexbidv 2968 . . 3
6 df-iun 4332 . . 3
75, 6elab2g 3248 . 2
81, 3, 7pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  e.wcel 1818  E.wrex 2808   cvv 3109  U_ciun 4330
This theorem is referenced by:  iuncom  4337  iuncom4  4338  iunconst  4339  iuniin  4341  iunss1  4342  ss2iun  4346  dfiun2g  4362  ssiun  4372  ssiun2  4373  iunab  4376  iun0  4386  0iun  4387  iunn0  4390  iunin2  4394  iundif2  4397  iindif2  4399  iunxsng  4409  iunun  4411  iunxun  4412  iunxiun  4413  iunpwss  4420  disjiun  4442  disjxiun  4449  triun  4558  otiunsndisj  4758  xpiundi  5059  xpiundir  5060  iunxpf  5156  cnvuni  5194  dmiun  5216  dmuni  5217  rniun  5421  xpdifid  5440  dfco2  5511  dfco2a  5512  coiun  5522  imaiun  6157  eluniima  6162  iunpw  6614  fun11iun  6760  opabex3d  6778  opabex3  6779  onoviun  7033  smoiun  7051  oalimcl  7228  oaass  7229  oarec  7230  omordlim  7245  omlimcl  7246  omeulem1  7250  oeordi  7255  oelimcl  7268  oeeulem  7269  oaabs2  7313  omabs  7315  dffi3  7911  ixpiunwdom  8038  trcl  8180  r1ordg  8217  r1pwss  8223  rankr1ai  8237  r1elss  8245  fseqenlem2  8427  fseqdom  8428  infpwfien  8464  cardaleph  8491  ackbij2  8644  cfsmolem  8671  alephsing  8677  hsmexlem2  8828  axdc3lem2  8852  ac6c4  8882  ttukeylem6  8915  iunfo  8935  iundom2g  8936  konigthlem  8964  alephreg  8978  pwcfsdom  8979  pwfseqlem3  9059  inar1  9174  inatsk  9177  fsuppmapnn0fiub  12097  wrdval  12551  fsum2dlem  13585  fsumcom2  13589  fsumiun  13635  fprod2dlem  13784  fprodcom2  13788  prmreclem5  14438  imasaddfnlem  14925  imasvscafn  14934  efgs1b  16754  efgsfo  16757  frgpnabllem1  16877  lssats2  17646  lbsextlem2  17805  lbsextlem3  17806  islpidl  17894  iunocv  18712  pmatcoe1fsupp  19202  iunconlem  19928  iuncon  19929  locfincmp  20027  alexsubALTlem3  20549  ptcmplem3  20554  imasdsf1olem  20876  zcld  21318  ovolfioo  21879  ovolficc  21880  ovoliunlem2  21914  ovoliunnul  21918  volfiniun  21957  iundisj  21958  iunmbl2  21967  volsup2  22014  vitalilem2  22018  ismbf3d  22061  mbfaddlem  22067  mbfsup  22071  i1faddlem  22100  i1fmullem  22101  elaa  22712  2spotiundisj  25062  usgreg2spot  25067  numclwwlkun  25079  ssiun3  27426  iunpreima  27432  iundisjf  27448  unipreima  27484  ofpreima  27507  iundisjfi  27601  locfinreflem  27843  eulerpartlemgh  28317  dstfrvunirn  28413  mclsppslem  28943  dfrtrclrec2  29066  eltrpred  29309  dftrpred3g  29316  trpredrec  29321  wfrlem9  29351  frrlem5e  29395  nofulllem5  29466  colinearex  29710  rabiun  30036  iundif1  30037  volsupnfl  30059  dvtanlem  30064  neibastop2lem  30178  istotbnd3  30267  sstotbnd  30271  sstotbnd3  30272  prdstotbnd  30290  cntotbnd  30292  heiborlem3  30309  heibor  30317  dvnprodlem1  31743  dvnprodlem2  31744  fourierdlem80  31969  otiunsndisjX  32301  iunconlem2  33735  bnj1405  33895  bnj916  33991  bnj983  34009  bnj1398  34090  bnj1417  34097  bnj1498  34117  pclfinN  35624  pclcmpatN  35625  lcfrvalsnN  37268  lcfrlem5  37273  lcfrlem6  37274  lcfrlem16  37285  lcfrlem27  37296  lcfrlem37  37306  lcfr  37312  mapdrvallem2  37372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-v 3111  df-iun 4332
  Copyright terms: Public domain W3C validator