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 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  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  7697  fiun  7867  f1iun  7868  opabex3d  7890  opabex3rd  7891  opabex3  7892  wfrdmclOLD  8255  onoviun  8281  smoiun  8299  oalimcl  8499  oaass  8500  oarec  8501  omordlim  8516  omlimcl  8517  omeulem1  8521  oelimcl  8539  oeeulem  8540  oaabs2  8587  omabs  8589  dffi3  9325  ixpiunwdom  9484  ttrclselem2  9620  trcl  9622  r1ordg  9672  r1pwss  9678  rankr1ai  9692  r1elss  9700  fseqenlem2  9919  infpwfien  9956  cardaleph  9983  ackbij2  10137  cfsmolem  10164  alephsing  10170  hsmexlem2  10321  ac6c4  10375  ttukeylem6  10408  iunfo  10433  iundom2g  10434  konigthlem  10462  alephreg  10476  pwcfsdom  10477  pwfseqlem3  10554  inar1  10669  inatsk  10672  fsuppmapnn0fiub  13850  wrdval  14359  s3iunsndisj  14813  dfrtrclrec2  14903  fsum2dlem  15615  fsumcom2  15619  fsumiun  15666  fprod2dlem  15823  fprodcom2  15827  prmreclem5  16752  imasaddfnlem  17370  imasvscafn  17379  smndex1basss  18675  smndex1mgm  18677  smndex1mndlem  18679  smndex1n0mnd  18682  efgsfo  19480  frgpnabllem1  19610  lssats2  20414  lbsextlem2  20573  lbsextlem3  20574  islpidl  20669  iunocv  21038  iunconnlem  22730  iunconn  22731  locfincmp  22829  alexsubALTlem3  23352  ptcmplem3  23357  imasdsf1olem  23678  zcld  24128  ovolfioo  24783  ovolficc  24784  ovoliunlem2  24819  ovoliunnul  24823  volfiniun  24863  iundisj  24864  iunmbl2  24873  volsup2  24921  vitalilem2  24925  ismbf3d  24970  mbfaddlem  24976  mbfsup  24980  i1faddlem  25009  i1fmullem  25010  elaa  25628  oldlim  27167  numedglnl  27924  clwwlknun  28885  fusgreg2wsp  29109  iunin1f  31305  ssiun3  31306  iunpreima  31312  iundisjf  31336  unipreima  31389  aciunf1lem  31407  ofpreima  31410  iundisjfi  31525  fsumiunle  31551  gsumpart  31723  elirng  32180  irngnzply1  32185  locfinreflem  32233  esum2dlem  32503  esum2d  32504  esumiun  32505  eulerpartlemgh  32790  dstfrvunirn  32886  reprsuc  33040  reprdifc  33052  bnj1405  33260  bnj916  33357  bnj983  33375  bnj1398  33458  bnj1417  33465  bnj1498  33485  fmlan0  33797  mclsppslem  33989  colinearex  34583  neibastop2lem  34770  rdgellim  35785  exrecfnlem  35788  rabiun  35989  iundif1  35990  volsupnfl  36061  istotbnd3  36168  sstotbnd  36172  sstotbnd3  36173  prdstotbnd  36191  cntotbnd  36193  heiborlem3  36210  heibor  36218  pclfinN  38301  pclcmpatN  38302  lcfrvalsnN  39942  lcfrlem5  39947  lcfrlem6  39948  lcfrlem16  39959  lcfrlem27  39970  lcfrlem37  39980  lcfr  39986  mapdrvallem2  40046  cnviun  41833  imaiun1  41834  coiun1  41835  ss2iundf  41842  eliunov2  41862  iunconnlem2  43128  iunincfi  43215  eliuniin  43220  eliuniin2  43241  eliunid  43271  iindif2f  43286  unirnmap  43334  unirnmapsn  43340  ssmapsn  43342  iunmapsn  43343  iuneqfzuzlem  43473  allbutfi  43533  fsumiunss  43717  fnlimfvre  43816  cnrefiisplem  43971  dvnprodlem1  44088  dvnprodlem2  44089  fourierdlem80  44328  sge0iunmptlemfi  44555  sge0iunmptlemre  44557  sge0iunmpt  44560  iundjiun  44602  meaiininclem  44628  hoicvr  44690  hoidmv1lelem3  44735  hoidmv1le  44736  hoidmvlelem3  44739  hspmbllem2  44769  opnvonmbllem2  44775  iunhoiioolem  44817  smfaddlem1  44905  smflimlem2  44914  smfmullem4  44936  smflimmpt  44952  smflimsuplem7  44968  smflimsuplem8  44969  smflimsupmpt  44971  smfliminfmpt  44974  fsupdm  44984  finfdm  44988  fsetsniunop  45184  otiunsndisjX  45412  iccpartiun  45527  iunord  47022
  Copyright terms: Public domain W3C validator