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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2142  ∃wrex 3088  Vcvv 3454  ∪ ciun 4955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3456  df-iun 4957

This theorem is used 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  5502  xpiundi  5731  xpiundir  5732  iunxpf  5833  cnvuni  5875  dmiun  5902  dmuni  5903  rniun  6144  xpdifid  6164  xpdifcnvepel  6165  dfco2  6245  dfco2a  6246  coiun  6257  imaiun  7243  eluniima  7248  iunpw  7768  fiun  7938  f1iun  7939  opabex3d  7960  opabex3rd  7961  opabex3  7962  onoviun  8328  smoiun  8346  oalimcl  8543  oaass  8544  oarec  8545  omordlim  8560  omlimcl  8561  omeulem1  8565  oelimcl  8584  oeeulem  8585  oaabs2  8633  omabs  8635  dffi3  9389  ixpiunwdom  9550  ttrclselem2  9693  trcl  9695  r1ordg  9748  r1pwss  9754  rankr1ai  9768  r1elss  9776  fseqenlem2  10016  infpwfien  10053  cardaleph  10080  ackbij2  10232  cfsmolem  10260  alephsing  10266  hsmexlem2  10417  ac6c4  10471  ttukeylem6  10504  iunfo  10529  iundom2g  10530  konigthlem  10559  alephreg  10573  pwcfsdom  10574  pwfseqlem3  10651  inar1  10766  inatsk  10769  fsuppmapnn0fiub  14034  wrdval  14560  s3iunsndisj  15012  dfrtrclrec2  15102  fsum2dlem  15828  fsumcom2  15832  fsumiun  15880  fprod2dlem  16041  fprodcom2  16045  prmreclem5  16986  imasaddfnlem  17588  imasvscafn  17597  smndex1basss  18973  smndex1mgm  18975  smndex1mndlem  18977  smndex1n0mnd  18980  efgsfo  19815  frgpnabllem1  19949  lssats2  21132  lbsextlem2  21294  lbsextlem3  21295  islpidl  21504  pzriprnglem10  21651  pzriprnglem12  21653  pzriprnglem13  21654  pzriprnglem14  21655  iunocv  21842  iunconnlem  23595  iunconn  23596  locfincmp  23694  alexsubALTlem3  24217  ptcmplem3  24222  imasdsf1olem  24541  zcld  24982  ovolfioo  25637  ovolficc  25638  ovoliunlem2  25673  ovoliunnul  25677  volfiniun  25717  iundisj  25718  iunmbl2  25727  volsup2  25775  vitalilem2  25779  ismbf3d  25824  mbfaddlem  25830  mbfsup  25834  i1faddlem  25863  i1fmullem  25864  elaa  26488  oldlim  28091  precsexlem10  28420  precsexlem11  28421  numedglnl  29505  clwwlknun  30474  fusgreg2wsp  30698  iunin1f  32913  ssiun3  32914  iunpreima  32920  iundisjf  32945  unipreima  32999  aciunf1lem  33018  ofpreima  33021  iundisjfi  33152  fsumiunle  33184  gsumpart  33392  gsumwrd2dccatlem  33406  elirng  34085  irngnzply1  34090  irngnminplynz  34111  constrconj  34144  locfinreflem  34239  esum2dlem  34491  esum2d  34492  esumiun  34493  eulerpartlemgh  34777  dstfrvunirn  34874  reprsuc  35011  reprdifc  35023  bnj1405  35233  bnj916  35330  bnj983  35348  bnj1398  35431  bnj1417  35438  bnj1498  35458  fmlan0  35891  mclsppslem  36083  colinearex  36560  neibastop2lem  36899  weiunlem  37002  ttctr  37032  rdgellim  38050  exrecfnlem  38053  rabiun  38272  iundif1  38273  volsupnfl  38344  istotbnd3  38450  sstotbnd  38454  sstotbnd3  38455  prdstotbnd  38473  cntotbnd  38475  heiborlem3  38492  heibor  38500  pclfinN  40702  pclcmpatN  40703  lcfrvalsnN  42343  lcfrlem5  42348  lcfrlem6  42349  lcfrlem16  42360  lcfrlem27  42371  lcfrlem37  42381  lcfr  42387  mapdrvallem2  42447  grpods  42989  cnviun  44404  imaiun1  44405  coiun1  44406  ss2iundf  44413  eliunov2  44433  iunconnlem2  45671  iunincfi  45840  eliuniin  45845  eliuniin2  45866  eliunid  45893  iindif2f  45906  unirnmap  45952  unirnmapsn  45958  ssmapsn  45960  iunmapsn  45961  iuneqfzuzlem  46078  allbutfi  46136  fsumiunss  46319  fnlimfvre  46416  cnrefiisplem  46571  dvnprodlem1  46688  dvnprodlem2  46689  fourierdlem80  46928  sge0iunmptlemfi  47155  sge0iunmptlemre  47157  sge0iunmpt  47160  iundjiun  47202  meaiininclem  47228  hoidmv1lelem3  47335  hoidmv1le  47336  hoidmvlelem3  47339  hspmbllem2  47369  opnvonmbllem2  47375  iunhoiioolem  47417  smfaddlem1  47505  smflimlem2  47514  smfmullem4  47536  smflimmpt  47552  smflimsuplem7  47568  smflimsuplem8  47569  smflimsupmpt  47571  smfliminfmpt  47574  fsupdm  47584  finfdm  47588  fsetsniunop  47814  otiunsndisjX  48044  iccpartiun  48211  stgredgiun  48751  iunord  50482