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

Theorem eliun 4460
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 3185 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3185 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3011 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2676 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3034 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4457 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3322 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 367 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  wcel 1977  wrex 2897  Vcvv 3173   ciun 4455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-iun 4457
This theorem is referenced by:  eliuni  4462  iuncom  4463  iuncom4  4464  iunconst  4465  iuniin  4467  iunss1  4468  ss2iun  4472  dfiun2g  4488  ssiun  4498  ssiun2  4499  iunab  4502  iun0  4512  0iun  4513  iunn0  4516  iunin2  4520  iundif2  4523  iindif2  4525  iunxsng  4538  iunun  4540  iunxun  4541  iunxdif3  4542  iunxiun  4544  iunpwss  4551  disjiun  4573  disjxiun  4579  disjxiunOLD  4580  triun  4694  otiunsndisj  4905  xpiundi  5096  xpiundir  5097  iunxpf  5192  cnvuni  5231  dmiun  5255  dmuni  5256  rniun  5462  xpdifid  5481  dfco2  5551  dfco2a  5552  coiun  5562  imaiun  6407  eluniima  6412  iunpw  6870  fun11iun  7019  opabex3d  7037  opabex3  7038  wfrdmcl  7310  onoviun  7327  smoiun  7345  oalimcl  7527  oaass  7528  oarec  7529  omordlim  7544  omlimcl  7545  omeulem1  7549  oelimcl  7567  oeeulem  7568  oaabs2  7612  omabs  7614  dffi3  8220  ixpiunwdom  8379  trcl  8487  r1ordg  8524  r1pwss  8530  rankr1ai  8544  r1elss  8552  fseqenlem2  8731  infpwfien  8768  cardaleph  8795  ackbij2  8948  cfsmolem  8975  alephsing  8981  hsmexlem2  9132  ac6c4  9186  ttukeylem6  9219  iunfo  9240  iundom2g  9241  konigthlem  9269  alephreg  9283  pwcfsdom  9284  pwfseqlem3  9361  inar1  9476  inatsk  9479  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  wrdval  13163  s3iunsndisj  13555  dfrtrclrec2  13645  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumiun  14394  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  prmreclem5  15462  imasaddfnlem  16011  imasvscafn  16020  efgsfo  17975  frgpnabllem1  18099  lssats2  18821  lbsextlem2  18980  lbsextlem3  18981  islpidl  19067  iunocv  19844  iunconlem  21040  iuncon  21041  locfincmp  21139  alexsubALTlem3  21663  ptcmplem3  21668  imasdsf1olem  21988  zcld  22424  ovolfioo  23043  ovolficc  23044  ovoliunlem2  23078  ovoliunnul  23082  volfiniun  23122  iundisj  23123  iunmbl2  23132  volsup2  23179  vitalilem2  23184  ismbf3d  23227  mbfaddlem  23233  mbfsup  23237  i1faddlem  23266  i1fmullem  23267  elaa  23875  2spotiundisj  26589  usgreg2spot  26594  numclwwlkun  26606  iunin1f  28757  iunxsngf  28758  ssiun3  28759  iunpreima  28765  iundisjf  28784  unipreima  28826  aciunf1lem  28844  ofpreima  28848  iundisjfi  28942  locfinreflem  29235  esum2dlem  29481  esum2d  29482  esumiun  29483  eulerpartlemgh  29767  dstfrvunirn  29863  bnj1405  30161  bnj916  30257  bnj983  30275  bnj1398  30356  bnj1417  30363  bnj1498  30383  mclsppslem  30734  eltrpred  30970  dftrpred3g  30977  trpredrec  30982  frrlem5e  31032  nofulllem5  31105  colinearex  31337  neibastop2lem  31525  rabiun  32552  iundif1  32553  volsupnfl  32624  istotbnd3  32740  sstotbnd  32744  sstotbnd3  32745  prdstotbnd  32763  cntotbnd  32765  heiborlem3  32782  heibor  32790  pclfinN  34204  pclcmpatN  34205  lcfrvalsnN  35848  lcfrlem5  35853  lcfrlem6  35854  lcfrlem16  35865  lcfrlem27  35876  lcfrlem37  35886  lcfr  35892  mapdrvallem2  35952  cnviun  36961  imaiun1  36962  coiun1  36963  ss2iundf  36970  eliunov2  36990  iunconlem2  38193  iunxsngf2  38255  iunincfi  38300  eliuniin  38307  eliuniin2  38335  unirnmap  38395  unirnmapsn  38401  ssmapsn  38403  iunmapsn  38404  iuneqfzuzlem  38491  allbutfi  38557  fsumiunss  38642  fnlimfvre  38741  dvnprodlem1  38836  dvnprodlem2  38837  fourierdlem80  39079  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  iundjiun  39353  meaiininclem  39376  hoicvr  39438  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem3  39487  hspmbllem2  39517  opnvonmbllem2  39523  iunhoiioolem  39566  smfaddlem1  39649  smflimlem2  39658  smfmullem4  39679  iccpartiun  39972  otiunsndisjX  40317  2wspiundisj  41166  clwwlksnun  41281  fusgreg2wsp  41500  iunord  42220
  Copyright terms: Public domain W3C validator