Theorem eliun 4954

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.

Step	Hyp	Ref	Expression
1		elex 3476	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3476	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3160	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2851	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3187	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4952	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3640	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 208   = wceq 1561   ∈ wcel 2143  ∃wrex 3087  Vcvv 3455  ∪ ciun 4950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3088  df-v 3457  df-iun 4952

This theorem is referenced by:  eliuni  4956  eliund  4957  iuncom  4958  iuncom4  4959  iunconst  4960  iuneqconst  4962  iuniin  4963  iinssiun  4964  iunss1  4965  ss2iun  4969  nfiu1  4986  iunssf  5001  iunss  5003  ssiun  5005  ssiun2  5006  iunab  5010  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  5089  disjiund  5092  disjxiun  5098  triun  5223  otiunsndisj  5490  xpiundi  5719  xpiundir  5720  iunxpf  5821  cnvuni  5863  dmiun  5890  dmuni  5891  rniun  6132  xpdifid  6153  xpdifcnvepel  6154  dfco2  6232  dfco2a  6233  coiun  6244  imaiun  7229  eluniima  7234  iunpw  7754  fiun  7924  f1iun  7925  opabex3d  7946  opabex3rd  7947  opabex3  7948  onoviun  8314  smoiun  8332  oalimcl  8529  oaass  8530  oarec  8531  omordlim  8546  omlimcl  8547  omeulem1  8551  oelimcl  8570  oeeulem  8571  oaabs2  8619  omabs  8621  dffi3  9375  ixpiunwdom  9536  ttrclselem2  9679  trcl  9681  r1ordg  9734  r1pwss  9740  rankr1ai  9754  r1elss  9762  fseqenlem2  9993  infpwfien  10030  cardaleph  10057  ackbij2  10209  cfsmolem  10238  alephsing  10244  hsmexlem2  10395  ac6c4  10449  ttukeylem6  10482  iunfo  10507  iundom2g  10508  konigthlem  10537  alephreg  10551  pwcfsdom  10552  pwfseqlem3  10629  inar1  10744  inatsk  10747  fsuppmapnn0fiub  14014  wrdval  14539  s3iunsndisj  14991  dfrtrclrec2  15081  fsum2dlem  15807  fsumcom2  15811  fsumiun  15859  fprod2dlem  16020  fprodcom2  16024  prmreclem5  16966  imasaddfnlem  17568  imasvscafn  17577  smndex1basss  18952  smndex1mgm  18954  smndex1mndlem  18956  smndex1n0mnd  18959  efgsfo  19789  frgpnabllem1  19923  lssats2  21074  lbsextlem2  21236  lbsextlem3  21237  islpidl  21402  pzriprnglem10  21549  pzriprnglem12  21551  pzriprnglem13  21552  pzriprnglem14  21553  iunocv  21740  iunconnlem  23494  iunconn  23495  locfincmp  23593  alexsubALTlem3  24116  ptcmplem3  24121  imasdsf1olem  24440  zcld  24881  ovolfioo  25536  ovolficc  25537  ovoliunlem2  25572  ovoliunnul  25576  volfiniun  25616  iundisj  25617  iunmbl2  25626  volsup2  25674  vitalilem2  25678  ismbf3d  25723  mbfaddlem  25729  mbfsup  25733  i1faddlem  25762  i1fmullem  25763  elaa  26387  oldlim  27987  precsexlem10  28316  precsexlem11  28317  numedglnl  29352  clwwlknun  30321  fusgreg2wsp  30545  iunin1f  32763  ssiun3  32764  iunpreima  32770  iundisjf  32795  unipreima  32851  aciunf1lem  32870  ofpreima  32873  iundisjfi  33004  fsumiunle  33037  gsumpart  33249  gsumwrd2dccatlem  33263  elirng  33985  irngnzply1  33990  irngnminplynz  34011  constrconj  34044  locfinreflem  34139  esum2dlem  34391  esum2d  34392  esumiun  34393  eulerpartlemgh  34677  dstfrvunirn  34774  reprsuc  34911  reprdifc  34923  bnj1405  35133  bnj916  35230  bnj983  35248  bnj1398  35331  bnj1417  35338  bnj1498  35358  fmlan0  35746  mclsppslem  35938  colinearex  36415  neibastop2lem  36725  weiunlem  36828  ttctr  36858  rdgellim  37875  exrecfnlem  37878  rabiun  38097  iundif1  38098  volsupnfl  38169  istotbnd3  38275  sstotbnd  38279  sstotbnd3  38280  prdstotbnd  38298  cntotbnd  38300  heiborlem3  38317  heibor  38325  pclfinN  40529  pclcmpatN  40530  lcfrvalsnN  42170  lcfrlem5  42175  lcfrlem6  42176  lcfrlem16  42187  lcfrlem27  42198  lcfrlem37  42208  lcfr  42214  mapdrvallem2  42274  grpods  42816  cnviun  44231  imaiun1  44232  coiun1  44233  ss2iundf  44240  eliunov2  44260  iunconnlem2  45501  iunincfi  45663  eliuniin  45668  eliuniin2  45689  eliunid  45716  iindif2f  45729  unirnmap  45775  unirnmapsn  45781  ssmapsn  45783  iunmapsn  45784  iuneqfzuzlem  45901  allbutfi  45959  fsumiunss  46142  fnlimfvre  46239  cnrefiisplem  46394  dvnprodlem1  46511  dvnprodlem2  46512  fourierdlem80  46751  sge0iunmptlemfi  46978  sge0iunmptlemre  46980  sge0iunmpt  46983  iundjiun  47025  meaiininclem  47051  hoidmv1lelem3  47158  hoidmv1le  47159  hoidmvlelem3  47162  hspmbllem2  47192  opnvonmbllem2  47198  iunhoiioolem  47240  smfaddlem1  47328  smflimlem2  47337  smfmullem4  47359  smflimmpt  47375  smflimsuplem7  47391  smflimsuplem8  47392  smflimsupmpt  47394  smfliminfmpt  47397  fsupdm  47407  finfdm  47411  fsetsniunop  47634  otiunsndisjX  47864  iccpartiun  48031  stgredgiun  48571  iunord  50288