Theorem eliun 5019

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 3509	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3509	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3157	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2832	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3185	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 5017	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3696	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  ∃wrex 3076  Vcvv 3488  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-iun 5017

This theorem is referenced by:  eliuni  5021  iuncom  5022  iuncom4  5023  iunconst  5024  iuneqconst  5026  iuniin  5027  iinssiun  5028  iunss1  5029  ss2iun  5033  nfiu1  5050  dfiun2gOLD  5054  ssiun  5069  ssiun2  5070  iunab  5074  iun0  5085  0iun  5086  iunn0  5090  iunin2  5094  iundif2  5097  iindif2  5100  iunxsng  5113  iunxsngf  5115  iunun  5116  iunxun  5117  iunxdif3  5118  iunxiun  5120  iunpwss  5130  disjiun  5154  disjiund  5157  disjxiun  5163  triun  5298  otiunsndisj  5539  xpiundi  5770  xpiundir  5771  iunxpf  5873  cnvuni  5911  dmiun  5938  dmuni  5939  rniun  6179  xpdifid  6199  dfco2  6276  dfco2a  6277  coiun  6287  imaiun  7282  eluniima  7287  iunpw  7806  fiun  7983  f1iun  7984  opabex3d  8006  opabex3rd  8007  opabex3  8008  wfrdmclOLD  8373  onoviun  8399  smoiun  8417  oalimcl  8616  oaass  8617  oarec  8618  omordlim  8633  omlimcl  8634  omeulem1  8638  oelimcl  8656  oeeulem  8657  oaabs2  8705  omabs  8707  dffi3  9500  ixpiunwdom  9659  ttrclselem2  9795  trcl  9797  r1ordg  9847  r1pwss  9853  rankr1ai  9867  r1elss  9875  fseqenlem2  10094  infpwfien  10131  cardaleph  10158  ackbij2  10311  cfsmolem  10339  alephsing  10345  hsmexlem2  10496  ac6c4  10550  ttukeylem6  10583  iunfo  10608  iundom2g  10609  konigthlem  10637  alephreg  10651  pwcfsdom  10652  pwfseqlem3  10729  inar1  10844  inatsk  10847  fsuppmapnn0fiub  14042  wrdval  14565  s3iunsndisj  15017  dfrtrclrec2  15107  fsum2dlem  15818  fsumcom2  15822  fsumiun  15869  fprod2dlem  16028  fprodcom2  16032  prmreclem5  16967  imasaddfnlem  17588  imasvscafn  17597  smndex1basss  18940  smndex1mgm  18942  smndex1mndlem  18944  smndex1n0mnd  18947  efgsfo  19781  frgpnabllem1  19915  lssats2  21021  lbsextlem2  21184  lbsextlem3  21185  islpidl  21358  pzriprnglem10  21524  pzriprnglem12  21526  pzriprnglem13  21527  pzriprnglem14  21528  iunocv  21722  iunconnlem  23456  iunconn  23457  locfincmp  23555  alexsubALTlem3  24078  ptcmplem3  24083  imasdsf1olem  24404  zcld  24854  ovolfioo  25521  ovolficc  25522  ovoliunlem2  25557  ovoliunnul  25561  volfiniun  25601  iundisj  25602  iunmbl2  25611  volsup2  25659  vitalilem2  25663  ismbf3d  25708  mbfaddlem  25714  mbfsup  25718  i1faddlem  25747  i1fmullem  25748  elaa  26376  oldlim  27943  precsexlem10  28258  precsexlem11  28259  numedglnl  29179  clwwlknun  30144  fusgreg2wsp  30368  iunin1f  32580  ssiun3  32581  iunpreima  32587  iundisjf  32611  unipreima  32662  aciunf1lem  32680  ofpreima  32683  iundisjfi  32801  fsumiunle  32833  gsumpart  33038  elirng  33686  irngnzply1  33691  irngnminplynz  33705  constrconj  33735  locfinreflem  33786  esum2dlem  34056  esum2d  34057  esumiun  34058  eulerpartlemgh  34343  dstfrvunirn  34439  reprsuc  34592  reprdifc  34604  bnj1405  34812  bnj916  34909  bnj983  34927  bnj1398  35010  bnj1417  35017  bnj1498  35037  fmlan0  35359  mclsppslem  35551  colinearex  36024  neibastop2lem  36326  weiunlem2  36429  rdgellim  37342  exrecfnlem  37345  rabiun  37553  iundif1  37554  volsupnfl  37625  istotbnd3  37731  sstotbnd  37735  sstotbnd3  37736  prdstotbnd  37754  cntotbnd  37756  heiborlem3  37773  heibor  37781  pclfinN  39857  pclcmpatN  39858  lcfrvalsnN  41498  lcfrlem5  41503  lcfrlem6  41504  lcfrlem16  41515  lcfrlem27  41526  lcfrlem37  41536  lcfr  41542  mapdrvallem2  41602  grpods  42151  cnviun  43612  imaiun1  43613  coiun1  43614  ss2iundf  43621  eliunov2  43641  iunconnlem2  44906  iunincfi  44996  eliuniin  45001  eliuniin2  45022  eliunid  45052  iindif2f  45065  eliund  45068  unirnmap  45115  unirnmapsn  45121  ssmapsn  45123  iunmapsn  45124  iuneqfzuzlem  45249  allbutfi  45308  fsumiunss  45496  fnlimfvre  45595  cnrefiisplem  45750  dvnprodlem1  45867  dvnprodlem2  45868  fourierdlem80  46107  sge0iunmptlemfi  46334  sge0iunmptlemre  46336  sge0iunmpt  46339  iundjiun  46381  meaiininclem  46407  hoicvr  46469  hoidmv1lelem3  46514  hoidmv1le  46515  hoidmvlelem3  46518  hspmbllem2  46548  opnvonmbllem2  46554  iunhoiioolem  46596  smfaddlem1  46684  smflimlem2  46693  smfmullem4  46715  smflimmpt  46731  smflimsuplem7  46747  smflimsuplem8  46748  smflimsupmpt  46750  smfliminfmpt  46753  fsupdm  46763  finfdm  46767  fsetsniunop  46964  otiunsndisjX  47194  iccpartiun  47308  iunord  48768