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

Theorem eliun 4454
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 3184 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3184 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3010 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2675 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3033 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4451 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3321 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 366 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wcel 1976  wrex 2896  Vcvv 3172   ciun 4449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-v 3174  df-iun 4451
This theorem is referenced by:  eliuni  4456  iuncom  4457  iuncom4  4458  iunconst  4459  iuniin  4461  iunss1  4462  ss2iun  4466  dfiun2g  4482  ssiun  4492  ssiun2  4493  iunab  4496  iun0  4506  0iun  4507  iunn0  4510  iunin2  4514  iundif2  4517  iindif2  4519  iunxsng  4532  iunun  4534  iunxun  4535  iunxdif3  4536  iunxiun  4538  iunpwss  4545  disjiun  4567  disjxiun  4573  disjxiunOLD  4574  triun  4688  otiunsndisj  4896  xpiundi  5086  xpiundir  5087  iunxpf  5180  cnvuni  5219  dmiun  5242  dmuni  5243  rniun  5448  xpdifid  5467  dfco2  5537  dfco2a  5538  coiun  5548  imaiun  6385  eluniima  6390  iunpw  6847  fun11iun  6996  opabex3d  7014  opabex3  7015  wfrdmcl  7287  onoviun  7304  smoiun  7322  oalimcl  7504  oaass  7505  oarec  7506  omordlim  7521  omlimcl  7522  omeulem1  7526  oelimcl  7544  oeeulem  7545  oaabs2  7589  omabs  7591  dffi3  8197  ixpiunwdom  8356  trcl  8464  r1ordg  8501  r1pwss  8507  rankr1ai  8521  r1elss  8529  fseqenlem2  8708  infpwfien  8745  cardaleph  8772  ackbij2  8925  cfsmolem  8952  alephsing  8958  hsmexlem2  9109  ac6c4  9163  ttukeylem6  9196  iunfo  9217  iundom2g  9218  konigthlem  9246  alephreg  9260  pwcfsdom  9261  pwfseqlem3  9338  inar1  9453  inatsk  9456  fsuppmapnn0fiub  12607  fsuppmapnn0fiubOLD  12608  wrdval  13109  s3iunsndisj  13501  dfrtrclrec2  13591  fsum2dlem  14289  fsumcom2  14293  fsumcom2OLD  14294  fsumiun  14340  fprod2dlem  14495  fprodcom2  14499  fprodcom2OLD  14500  prmreclem5  15408  imasaddfnlem  15957  imasvscafn  15966  efgsfo  17921  frgpnabllem1  18045  lssats2  18767  lbsextlem2  18926  lbsextlem3  18927  islpidl  19013  iunocv  19786  iunconlem  20982  iuncon  20983  locfincmp  21081  alexsubALTlem3  21605  ptcmplem3  21610  imasdsf1olem  21929  zcld  22356  ovolfioo  22960  ovolficc  22961  ovoliunlem2  22995  ovoliunnul  22999  volfiniun  23039  iundisj  23040  iunmbl2  23049  volsup2  23096  vitalilem2  23101  ismbf3d  23144  mbfaddlem  23150  mbfsup  23154  i1faddlem  23183  i1fmullem  23184  elaa  23792  2spotiundisj  26355  usgreg2spot  26360  numclwwlkun  26372  iunin1f  28563  iunxsngf  28564  ssiun3  28565  iunpreima  28571  iundisjf  28590  unipreima  28632  aciunf1lem  28650  ofpreima  28654  iundisjfi  28748  locfinreflem  29041  esum2dlem  29287  esum2d  29288  esumiun  29289  eulerpartlemgh  29573  dstfrvunirn  29669  bnj1405  29967  bnj916  30063  bnj983  30081  bnj1398  30162  bnj1417  30169  bnj1498  30189  mclsppslem  30540  eltrpred  30776  dftrpred3g  30783  trpredrec  30788  frrlem5e  30838  nofulllem5  30911  colinearex  31143  neibastop2lem  31331  rabiun  32348  iundif1  32349  volsupnfl  32420  istotbnd3  32536  sstotbnd  32540  sstotbnd3  32541  prdstotbnd  32559  cntotbnd  32561  heiborlem3  32578  heibor  32586  pclfinN  34000  pclcmpatN  34001  lcfrvalsnN  35644  lcfrlem5  35649  lcfrlem6  35650  lcfrlem16  35661  lcfrlem27  35672  lcfrlem37  35682  lcfr  35688  mapdrvallem2  35748  cnviun  36757  imaiun1  36758  coiun1  36759  ss2iundf  36766  eliunov2  36786  iunconlem2  37989  iunxsngf2  38051  iunincfi  38096  eliuniin  38103  eliuniin2  38131  unirnmap  38191  unirnmapsn  38197  ssmapsn  38199  iunmapsn  38200  iuneqfzuzlem  38288  allbutfi  38354  fsumiunss  38439  fnlimfvre  38538  dvnprodlem1  38633  dvnprodlem2  38634  fourierdlem80  38876  sge0iunmptlemfi  39103  sge0iunmptlemre  39105  sge0iunmpt  39108  iundjiun  39150  meaiininclem  39173  hoicvr  39235  hoidmv1lelem3  39280  hoidmv1le  39281  hoidmvlelem3  39284  hspmbllem2  39314  opnvonmbllem2  39320  iunhoiioolem  39363  smfaddlem1  39446  smflimlem2  39455  smfmullem4  39476  iccpartiun  39770  otiunsndisjX  40125  2wspiundisj  41161  clwwlksnun  41276  fusgreg2wsp  41495
  Copyright terms: Public domain W3C validator