Theorem eliun 4997

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 3493	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3493	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3152	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2822	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3179	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4995	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3668	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  Vcvv 3475  ∪ ciun 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-iun 4995

This theorem is referenced by:  eliuni  4999  iuncom  5000  iuncom4  5001  iunconst  5002  iuneqconst  5004  iuniin  5005  iinssiun  5006  iunss1  5007  ss2iun  5011  dfiun2gOLD  5030  ssiun  5045  ssiun2  5046  iunab  5050  iun0  5061  0iun  5062  iunn0  5066  iunin2  5070  iundif2  5073  iindif2  5076  iunxsng  5089  iunxsngf  5091  iunun  5092  iunxun  5093  iunxdif3  5094  iunxiun  5096  iunpwss  5106  disjiun  5131  disjiund  5134  disjxiun  5141  triun  5276  otiunsndisj  5516  xpiundi  5741  xpiundir  5742  iunxpf  5843  cnvuni  5881  dmiun  5908  dmuni  5909  rniun  6139  xpdifid  6159  dfco2  6236  dfco2a  6237  coiun  6247  imaiun  7231  eluniima  7236  iunpw  7745  fiun  7916  f1iun  7917  opabex3d  7939  opabex3rd  7940  opabex3  7941  wfrdmclOLD  8304  onoviun  8330  smoiun  8348  oalimcl  8548  oaass  8549  oarec  8550  omordlim  8565  omlimcl  8566  omeulem1  8570  oelimcl  8588  oeeulem  8589  oaabs2  8636  omabs  8638  dffi3  9413  ixpiunwdom  9572  ttrclselem2  9708  trcl  9710  r1ordg  9760  r1pwss  9766  rankr1ai  9780  r1elss  9788  fseqenlem2  10007  infpwfien  10044  cardaleph  10071  ackbij2  10225  cfsmolem  10252  alephsing  10258  hsmexlem2  10409  ac6c4  10463  ttukeylem6  10496  iunfo  10521  iundom2g  10522  konigthlem  10550  alephreg  10564  pwcfsdom  10565  pwfseqlem3  10642  inar1  10757  inatsk  10760  fsuppmapnn0fiub  13943  wrdval  14454  s3iunsndisj  14902  dfrtrclrec2  14992  fsum2dlem  15703  fsumcom2  15707  fsumiun  15754  fprod2dlem  15911  fprodcom2  15915  prmreclem5  16840  imasaddfnlem  17461  imasvscafn  17470  smndex1basss  18773  smndex1mgm  18775  smndex1mndlem  18777  smndex1n0mnd  18780  efgsfo  19591  frgpnabllem1  19724  lssats2  20588  lbsextlem2  20749  lbsextlem3  20750  islpidl  20860  iunocv  21207  iunconnlem  22900  iunconn  22901  locfincmp  22999  alexsubALTlem3  23522  ptcmplem3  23527  imasdsf1olem  23848  zcld  24298  ovolfioo  24953  ovolficc  24954  ovoliunlem2  24989  ovoliunnul  24993  volfiniun  25033  iundisj  25034  iunmbl2  25043  volsup2  25091  vitalilem2  25095  ismbf3d  25140  mbfaddlem  25146  mbfsup  25150  i1faddlem  25179  i1fmullem  25180  elaa  25798  oldlim  27348  precsexlem10  27629  precsexlem11  27630  numedglnl  28371  clwwlknun  29332  fusgreg2wsp  29556  iunin1f  31755  ssiun3  31756  iunpreima  31762  iundisjf  31786  unipreima  31838  aciunf1lem  31856  ofpreima  31859  iundisjfi  31978  fsumiunle  32006  gsumpart  32178  elirng  32688  irngnzply1  32693  locfinreflem  32751  esum2dlem  33021  esum2d  33022  esumiun  33023  eulerpartlemgh  33308  dstfrvunirn  33404  reprsuc  33558  reprdifc  33570  bnj1405  33778  bnj916  33875  bnj983  33893  bnj1398  33976  bnj1417  33983  bnj1498  34003  fmlan0  34313  mclsppslem  34505  colinearex  34963  neibastop2lem  35150  rdgellim  36162  exrecfnlem  36165  rabiun  36366  iundif1  36367  volsupnfl  36438  istotbnd3  36545  sstotbnd  36549  sstotbnd3  36550  prdstotbnd  36568  cntotbnd  36570  heiborlem3  36587  heibor  36595  pclfinN  38677  pclcmpatN  38678  lcfrvalsnN  40318  lcfrlem5  40323  lcfrlem6  40324  lcfrlem16  40335  lcfrlem27  40346  lcfrlem37  40356  lcfr  40362  mapdrvallem2  40422  cnviun  42272  imaiun1  42273  coiun1  42274  ss2iundf  42281  eliunov2  42301  iunconnlem2  43567  iunincfi  43654  eliuniin  43659  eliuniin2  43680  eliunid  43710  iindif2f  43725  eliund  43728  unirnmap  43778  unirnmapsn  43784  ssmapsn  43786  iunmapsn  43787  iuneqfzuzlem  43917  allbutfi  43976  fsumiunss  44164  fnlimfvre  44263  cnrefiisplem  44418  dvnprodlem1  44535  dvnprodlem2  44536  fourierdlem80  44775  sge0iunmptlemfi  45002  sge0iunmptlemre  45004  sge0iunmpt  45007  iundjiun  45049  meaiininclem  45075  hoicvr  45137  hoidmv1lelem3  45182  hoidmv1le  45183  hoidmvlelem3  45186  hspmbllem2  45216  opnvonmbllem2  45222  iunhoiioolem  45264  smfaddlem1  45352  smflimlem2  45361  smfmullem4  45383  smflimmpt  45399  smflimsuplem7  45415  smflimsuplem8  45416  smflimsupmpt  45418  smfliminfmpt  45421  fsupdm  45431  finfdm  45435  fsetsniunop  45632  otiunsndisjX  45860  iccpartiun  45975  iunord  47561