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

Theorem eliun 4956
Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliun (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem eliun
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elex 3461 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3461 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3146 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2825 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3173 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4954 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3630 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 379 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wcel 2106  wrex 3071  Vcvv 3443   ciun 4952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3072  df-v 3445  df-iun 4954
This theorem is referenced by:  eliuni  4958  iuncom  4959  iuncom4  4960  iunconst  4961  iuneqconst  4963  iuniin  4964  iinssiun  4965  iunss1  4966  ss2iun  4970  dfiun2gOLD  4989  ssiun  5004  ssiun2  5005  iunab  5009  iun0  5020  0iun  5021  iunn0  5025  iunin2  5029  iundif2  5032  iindif2  5035  iunxsng  5048  iunxsngf  5050  iunun  5051  iunxun  5052  iunxdif3  5053  iunxiun  5055  iunpwss  5065  disjiun  5090  disjiund  5093  disjxiun  5100  triun  5235  otiunsndisj  5475  xpiundi  5700  xpiundir  5701  iunxpf  5802  cnvuni  5840  dmiun  5867  dmuni  5868  rniun  6098  xpdifid  6118  dfco2  6195  dfco2a  6196  coiun  6206  imaiun  7188  eluniima  7193  iunpw  7701  fiun  7871  f1iun  7872  opabex3d  7894  opabex3rd  7895  opabex3  7896  wfrdmclOLD  8259  onoviun  8285  smoiun  8303  oalimcl  8503  oaass  8504  oarec  8505  omordlim  8520  omlimcl  8521  omeulem1  8525  oelimcl  8543  oeeulem  8544  oaabs2  8591  omabs  8593  dffi3  9363  ixpiunwdom  9522  ttrclselem2  9658  trcl  9660  r1ordg  9710  r1pwss  9716  rankr1ai  9730  r1elss  9738  fseqenlem2  9957  infpwfien  9994  cardaleph  10021  ackbij2  10175  cfsmolem  10202  alephsing  10208  hsmexlem2  10359  ac6c4  10413  ttukeylem6  10446  iunfo  10471  iundom2g  10472  konigthlem  10500  alephreg  10514  pwcfsdom  10515  pwfseqlem3  10592  inar1  10707  inatsk  10710  fsuppmapnn0fiub  13888  wrdval  14397  s3iunsndisj  14845  dfrtrclrec2  14935  fsum2dlem  15647  fsumcom2  15651  fsumiun  15698  fprod2dlem  15855  fprodcom2  15859  prmreclem5  16784  imasaddfnlem  17402  imasvscafn  17411  smndex1basss  18707  smndex1mgm  18709  smndex1mndlem  18711  smndex1n0mnd  18714  efgsfo  19512  frgpnabllem1  19642  lssats2  20446  lbsextlem2  20605  lbsextlem3  20606  islpidl  20701  iunocv  21070  iunconnlem  22762  iunconn  22763  locfincmp  22861  alexsubALTlem3  23384  ptcmplem3  23389  imasdsf1olem  23710  zcld  24160  ovolfioo  24815  ovolficc  24816  ovoliunlem2  24851  ovoliunnul  24855  volfiniun  24895  iundisj  24896  iunmbl2  24905  volsup2  24953  vitalilem2  24957  ismbf3d  25002  mbfaddlem  25008  mbfsup  25012  i1faddlem  25041  i1fmullem  25042  elaa  25660  oldlim  27200  numedglnl  27981  clwwlknun  28942  fusgreg2wsp  29166  iunin1f  31362  ssiun3  31363  iunpreima  31369  iundisjf  31393  unipreima  31446  aciunf1lem  31464  ofpreima  31467  iundisjfi  31582  fsumiunle  31608  gsumpart  31780  elirng  32237  irngnzply1  32242  locfinreflem  32290  esum2dlem  32560  esum2d  32561  esumiun  32562  eulerpartlemgh  32847  dstfrvunirn  32943  reprsuc  33097  reprdifc  33109  bnj1405  33317  bnj916  33414  bnj983  33432  bnj1398  33515  bnj1417  33522  bnj1498  33542  fmlan0  33854  mclsppslem  34046  colinearex  34612  neibastop2lem  34799  rdgellim  35814  exrecfnlem  35817  rabiun  36018  iundif1  36019  volsupnfl  36090  istotbnd3  36197  sstotbnd  36201  sstotbnd3  36202  prdstotbnd  36220  cntotbnd  36222  heiborlem3  36239  heibor  36247  pclfinN  38330  pclcmpatN  38331  lcfrvalsnN  39971  lcfrlem5  39976  lcfrlem6  39977  lcfrlem16  39988  lcfrlem27  39999  lcfrlem37  40009  lcfr  40015  mapdrvallem2  40075  cnviun  41864  imaiun1  41865  coiun1  41866  ss2iundf  41873  eliunov2  41893  iunconnlem2  43159  iunincfi  43246  eliuniin  43251  eliuniin2  43272  eliunid  43302  iindif2f  43317  unirnmap  43365  unirnmapsn  43371  ssmapsn  43373  iunmapsn  43374  iuneqfzuzlem  43504  allbutfi  43564  fsumiunss  43748  fnlimfvre  43847  cnrefiisplem  44002  dvnprodlem1  44119  dvnprodlem2  44120  fourierdlem80  44359  sge0iunmptlemfi  44586  sge0iunmptlemre  44588  sge0iunmpt  44591  iundjiun  44633  meaiininclem  44659  hoicvr  44721  hoidmv1lelem3  44766  hoidmv1le  44767  hoidmvlelem3  44770  hspmbllem2  44800  opnvonmbllem2  44806  iunhoiioolem  44848  smfaddlem1  44936  smflimlem2  44945  smfmullem4  44967  smflimmpt  44983  smflimsuplem7  44999  smflimsuplem8  45000  smflimsupmpt  45002  smfliminfmpt  45005  fsupdm  45015  finfdm  45019  fsetsniunop  45215  otiunsndisjX  45443  iccpartiun  45558  iunord  47053
  Copyright terms: Public domain W3C validator