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

Theorem eliun 4556
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 3243 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3243 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3058 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2718 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3081 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4554 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3385 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 367 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  wcel 2030  wrex 2942  Vcvv 3231   ciun 4552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-iun 4554
This theorem is referenced by:  eliuni  4558  iuncom  4559  iuncom4  4560  iunconst  4561  iuniin  4563  iunss1  4564  ss2iun  4568  dfiun2g  4584  ssiun  4594  ssiun2  4595  iunab  4598  iun0  4608  0iun  4609  iunn0  4612  iunin2  4616  iundif2  4619  iindif2  4621  iunxsng  4634  iunun  4636  iunxun  4637  iunxdif3  4638  iunxiun  4640  iunpwss  4650  disjiun  4672  disjiund  4675  disjxiun  4681  disjxiunOLD  4682  triun  4799  otiunsndisj  5009  xpiundi  5207  xpiundir  5208  iunxpf  5303  cnvuni  5341  dmiun  5365  dmuni  5366  rniun  5578  xpdifid  5597  dfco2  5672  dfco2a  5673  coiun  5683  imaiun  6543  eluniima  6548  iunpw  7020  fun11iun  7168  opabex3d  7187  opabex3  7188  wfrdmcl  7468  onoviun  7485  smoiun  7503  oalimcl  7685  oaass  7686  oarec  7687  omordlim  7702  omlimcl  7703  omeulem1  7707  oelimcl  7725  oeeulem  7726  oaabs2  7770  omabs  7772  dffi3  8378  ixpiunwdom  8537  trcl  8642  r1ordg  8679  r1pwss  8685  rankr1ai  8699  r1elss  8707  fseqenlem2  8886  infpwfien  8923  cardaleph  8950  ackbij2  9103  cfsmolem  9130  alephsing  9136  hsmexlem2  9287  ac6c4  9341  ttukeylem6  9374  iunfo  9399  iundom2g  9400  konigthlem  9428  alephreg  9442  pwcfsdom  9443  pwfseqlem3  9520  inar1  9635  inatsk  9638  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  wrdval  13340  s3iunsndisj  13753  dfrtrclrec2  13841  fsum2dlem  14545  fsumcom2  14549  fsumcom2OLD  14550  fsumiun  14597  fprod2dlem  14754  fprodcom2  14758  fprodcom2OLD  14759  prmreclem5  15671  imasaddfnlem  16235  imasvscafn  16244  efgsfo  18198  frgpnabllem1  18322  lssats2  19048  lbsextlem2  19207  lbsextlem3  19208  islpidl  19294  iunocv  20073  iunconnlem  21278  iunconn  21279  locfincmp  21377  alexsubALTlem3  21900  ptcmplem3  21905  imasdsf1olem  22225  zcld  22663  ovolfioo  23282  ovolficc  23283  ovoliunlem2  23317  ovoliunnul  23321  volfiniun  23361  iundisj  23362  iunmbl2  23371  volsup2  23419  vitalilem2  23423  ismbf3d  23466  mbfaddlem  23472  mbfsup  23476  i1faddlem  23505  i1fmullem  23506  elaa  24116  numedglnl  26084  clwwlknun  27087  clwwlknunOLD  27091  fusgreg2wsp  27316  iunin1f  29500  iunxsngf  29501  ssiun3  29502  iinssiun  29503  iunpreima  29509  iundisjf  29528  unipreima  29574  aciunf1lem  29590  ofpreima  29593  iundisjfi  29683  fsumiunle  29703  locfinreflem  30035  esum2dlem  30282  esum2d  30283  esumiun  30284  eulerpartlemgh  30568  dstfrvunirn  30664  reprsuc  30821  reprdifc  30833  bnj1405  31033  bnj916  31129  bnj983  31147  bnj1398  31228  bnj1417  31235  bnj1498  31255  mclsppslem  31606  eltrpred  31850  dftrpred3g  31857  trpredrec  31862  frrlem5e  31913  colinearex  32292  neibastop2lem  32480  rabiun  33512  iundif1  33513  volsupnfl  33584  istotbnd3  33700  sstotbnd  33704  sstotbnd3  33705  prdstotbnd  33723  cntotbnd  33725  heiborlem3  33742  heibor  33750  pclfinN  35504  pclcmpatN  35505  lcfrvalsnN  37147  lcfrlem5  37152  lcfrlem6  37153  lcfrlem16  37164  lcfrlem27  37175  lcfrlem37  37185  lcfr  37191  mapdrvallem2  37251  cnviun  38259  imaiun1  38260  coiun1  38261  ss2iundf  38268  eliunov2  38288  iunconnlem2  39485  iunxsngf2  39544  iunincfi  39586  eliuniin  39593  eliuniin2  39617  eliunid  39656  unirnmap  39714  unirnmapsn  39720  ssmapsn  39722  iunmapsn  39723  iuneqfzuzlem  39863  allbutfi  39929  fsumiunss  40125  fnlimfvre  40224  cnrefiisplem  40373  dvnprodlem1  40479  dvnprodlem2  40480  fourierdlem80  40721  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0iunmpt  40953  iundjiun  40995  meaiininclem  41021  hoicvr  41083  hoidmv1lelem3  41128  hoidmv1le  41129  hoidmvlelem3  41132  hspmbllem2  41162  opnvonmbllem2  41168  iunhoiioolem  41210  smfaddlem1  41292  smflimlem2  41301  smfmullem4  41322  smflimmpt  41337  smflimsuplem7  41353  smflimsuplem8  41354  smflimsupmpt  41356  smfliminfmpt  41359  otiunsndisjX  41621  iccpartiun  41695  iunord  42747
  Copyright terms: Public domain W3C validator