Theorem eliun 4959

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 3474	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3474	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3160	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2849	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3187	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4957	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3638	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 381	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 209   = wceq 1568   ∈ wcel 2141  ∃wrex 3087  Vcvv 3453  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3455  df-iun 4957

This theorem is referenced by:  eliuni  4961  eliund  4962  iuncom  4963  iuncom4  4964  iunconst  4965  iuneqconst  4967  iuniin  4968  iinssiun  4969  iunss1  4970  ss2iun  4974  nfiu1  4991  iunssf  5006  iunss  5008  ssiun  5010  ssiun2  5011  iunab  5015  iun0  5025  0iun  5026  iunn0  5030  iunin2  5034  iundif2  5037  iindif2  5042  iunxsng  5055  iunxsngf  5057  iunun  5058  iunxun  5059  iunxdif3  5060  iunxiun  5062  iunpwss  5072  disjiun  5096  disjiund  5099  disjxiun  5105  triun  5232  otiunsndisj  5503  xpiundi  5732  xpiundir  5733  iunxpf  5834  cnvuni  5876  dmiun  5903  dmuni  5904  rniun  6145  xpdifid  6165  xpdifcnvepel  6166  dfco2  6246  dfco2a  6247  coiun  6258  imaiun  7243  eluniima  7248  iunpw  7769  fiun  7939  f1iun  7940  opabex3d  7961  opabex3rd  7962  opabex3  7963  onoviun  8329  smoiun  8347  oalimcl  8544  oaass  8545  oarec  8546  omordlim  8561  omlimcl  8562  omeulem1  8566  oelimcl  8585  oeeulem  8586  oaabs2  8634  omabs  8636  dffi3  9390  ixpiunwdom  9551  ttrclselem2  9694  trcl  9696  r1ordg  9749  r1pwss  9755  rankr1ai  9769  r1elss  9777  fseqenlem2  10008  infpwfien  10045  cardaleph  10072  ackbij2  10224  cfsmolem  10253  alephsing  10259  hsmexlem2  10410  ac6c4  10464  ttukeylem6  10497  iunfo  10522  iundom2g  10523  konigthlem  10552  alephreg  10566  pwcfsdom  10567  pwfseqlem3  10644  inar1  10759  inatsk  10762  fsuppmapnn0fiub  14026  wrdval  14552  s3iunsndisj  15004  dfrtrclrec2  15094  fsum2dlem  15820  fsumcom2  15824  fsumiun  15872  fprod2dlem  16033  fprodcom2  16037  prmreclem5  16979  imasaddfnlem  17581  imasvscafn  17590  smndex1basss  18966  smndex1mgm  18968  smndex1mndlem  18970  smndex1n0mnd  18973  efgsfo  19808  frgpnabllem1  19942  lssats2  21100  lbsextlem2  21262  lbsextlem3  21263  islpidl  21472  pzriprnglem10  21619  pzriprnglem12  21621  pzriprnglem13  21622  pzriprnglem14  21623  iunocv  21810  iunconnlem  23563  iunconn  23564  locfincmp  23662  alexsubALTlem3  24185  ptcmplem3  24190  imasdsf1olem  24509  zcld  24950  ovolfioo  25605  ovolficc  25606  ovoliunlem2  25641  ovoliunnul  25645  volfiniun  25685  iundisj  25686  iunmbl2  25695  volsup2  25743  vitalilem2  25747  ismbf3d  25792  mbfaddlem  25798  mbfsup  25802  i1faddlem  25831  i1fmullem  25832  elaa  26456  oldlim  28056  precsexlem10  28385  precsexlem11  28386  numedglnl  29460  clwwlknun  30429  fusgreg2wsp  30653  iunin1f  32868  ssiun3  32869  iunpreima  32875  iundisjf  32900  unipreima  32954  aciunf1lem  32973  ofpreima  32976  iundisjfi  33107  fsumiunle  33139  gsumpart  33349  gsumwrd2dccatlem  33363  elirng  34042  irngnzply1  34047  irngnminplynz  34068  constrconj  34101  locfinreflem  34196  esum2dlem  34448  esum2d  34449  esumiun  34450  eulerpartlemgh  34734  dstfrvunirn  34831  reprsuc  34968  reprdifc  34980  bnj1405  35190  bnj916  35287  bnj983  35305  bnj1398  35388  bnj1417  35395  bnj1498  35415  fmlan0  35837  mclsppslem  36029  colinearex  36506  neibastop2lem  36815  weiunlem  36918  ttctr  36948  rdgellim  37966  exrecfnlem  37969  rabiun  38188  iundif1  38189  volsupnfl  38260  istotbnd3  38366  sstotbnd  38370  sstotbnd3  38371  prdstotbnd  38389  cntotbnd  38391  heiborlem3  38408  heibor  38416  pclfinN  40620  pclcmpatN  40621  lcfrvalsnN  42261  lcfrlem5  42266  lcfrlem6  42267  lcfrlem16  42278  lcfrlem27  42289  lcfrlem37  42299  lcfr  42305  mapdrvallem2  42365  grpods  42907  cnviun  44324  imaiun1  44325  coiun1  44326  ss2iundf  44333  eliunov2  44353  iunconnlem2  45591  iunincfi  45760  eliuniin  45765  eliuniin2  45786  eliunid  45813  iindif2f  45826  unirnmap  45872  unirnmapsn  45878  ssmapsn  45880  iunmapsn  45881  iuneqfzuzlem  45998  allbutfi  46056  fsumiunss  46239  fnlimfvre  46336  cnrefiisplem  46491  dvnprodlem1  46608  dvnprodlem2  46609  fourierdlem80  46848  sge0iunmptlemfi  47075  sge0iunmptlemre  47077  sge0iunmpt  47080  iundjiun  47122  meaiininclem  47148  hoidmv1lelem3  47255  hoidmv1le  47256  hoidmvlelem3  47259  hspmbllem2  47289  opnvonmbllem2  47295  iunhoiioolem  47337  smfaddlem1  47425  smflimlem2  47434  smfmullem4  47456  smflimmpt  47472  smflimsuplem7  47488  smflimsuplem8  47489  smflimsupmpt  47491  smfliminfmpt  47494  fsupdm  47504  finfdm  47508  fsetsniunop  47731  otiunsndisjX  47961  iccpartiun  48128  stgredgiun  48668  iunord  50399