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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3447  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3449  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  dfiun2gOLD  4995  ssiun  5010  ssiun2  5011  iunab  5015  iun0  5026  0iun  5027  iunn0  5031  iunin2  5035  iundif2  5038  iindif2  5041  iunxsng  5054  iunxsngf  5056  iunun  5057  iunxun  5058  iunxdif3  5059  iunxiun  5061  iunpwss  5071  disjiun  5095  disjiund  5098  disjxiun  5104  triun  5229  otiunsndisj  5480  xpiundi  5709  xpiundir  5710  iunxpf  5812  cnvuni  5850  dmiun  5877  dmuni  5878  rniun  6120  xpdifid  6141  dfco2  6218  dfco2a  6219  coiun  6229  imaiun  7219  eluniima  7224  iunpw  7747  fiun  7921  f1iun  7922  opabex3d  7944  opabex3rd  7945  opabex3  7946  onoviun  8312  smoiun  8330  oalimcl  8524  oaass  8525  oarec  8526  omordlim  8541  omlimcl  8542  omeulem1  8546  oelimcl  8564  oeeulem  8565  oaabs2  8613  omabs  8615  dffi3  9382  ixpiunwdom  9543  ttrclselem2  9679  trcl  9681  r1ordg  9731  r1pwss  9737  rankr1ai  9751  r1elss  9759  fseqenlem2  9978  infpwfien  10015  cardaleph  10042  ackbij2  10195  cfsmolem  10223  alephsing  10229  hsmexlem2  10380  ac6c4  10434  ttukeylem6  10467  iunfo  10492  iundom2g  10493  konigthlem  10521  alephreg  10535  pwcfsdom  10536  pwfseqlem3  10613  inar1  10728  inatsk  10731  fsuppmapnn0fiub  13956  wrdval  14481  s3iunsndisj  14934  dfrtrclrec2  15024  fsum2dlem  15736  fsumcom2  15740  fsumiun  15787  fprod2dlem  15946  fprodcom2  15950  prmreclem5  16891  imasaddfnlem  17491  imasvscafn  17500  smndex1basss  18832  smndex1mgm  18834  smndex1mndlem  18836  smndex1n0mnd  18839  efgsfo  19669  frgpnabllem1  19803  lssats2  20906  lbsextlem2  21069  lbsextlem3  21070  islpidl  21235  pzriprnglem10  21400  pzriprnglem12  21402  pzriprnglem13  21403  pzriprnglem14  21404  iunocv  21590  iunconnlem  23314  iunconn  23315  locfincmp  23413  alexsubALTlem3  23936  ptcmplem3  23941  imasdsf1olem  24261  zcld  24702  ovolfioo  25368  ovolficc  25369  ovoliunlem2  25404  ovoliunnul  25408  volfiniun  25448  iundisj  25449  iunmbl2  25458  volsup2  25506  vitalilem2  25510  ismbf3d  25555  mbfaddlem  25561  mbfsup  25565  i1faddlem  25594  i1fmullem  25595  elaa  26224  oldlim  27798  precsexlem10  28118  precsexlem11  28119  numedglnl  29071  clwwlknun  30041  fusgreg2wsp  30265  iunin1f  32486  ssiun3  32487  iunpreima  32493  iundisjf  32518  unipreima  32567  aciunf1lem  32586  ofpreima  32589  iundisjfi  32719  fsumiunle  32754  gsumpart  32997  gsumwrd2dccatlem  33006  elirng  33681  irngnzply1  33686  irngnminplynz  33702  constrconj  33735  locfinreflem  33830  esum2dlem  34082  esum2d  34083  esumiun  34084  eulerpartlemgh  34369  dstfrvunirn  34466  reprsuc  34606  reprdifc  34618  bnj1405  34826  bnj916  34923  bnj983  34941  bnj1398  35024  bnj1417  35031  bnj1498  35051  fmlan0  35378  mclsppslem  35570  colinearex  36048  neibastop2lem  36348  weiunlem2  36451  rdgellim  37364  exrecfnlem  37367  rabiun  37587  iundif1  37588  volsupnfl  37659  istotbnd3  37765  sstotbnd  37769  sstotbnd3  37770  prdstotbnd  37788  cntotbnd  37790  heiborlem3  37807  heibor  37815  pclfinN  39894  pclcmpatN  39895  lcfrvalsnN  41535  lcfrlem5  41540  lcfrlem6  41541  lcfrlem16  41552  lcfrlem27  41563  lcfrlem37  41573  lcfr  41579  mapdrvallem2  41639  grpods  42182  cnviun  43639  imaiun1  43640  coiun1  43641  ss2iundf  43648  eliunov2  43668  iunconnlem2  44924  iunincfi  45088  eliuniin  45093  eliuniin2  45114  eliunid  45141  iindif2f  45154  unirnmap  45202  unirnmapsn  45208  ssmapsn  45210  iunmapsn  45211  iuneqfzuzlem  45330  allbutfi  45389  fsumiunss  45573  fnlimfvre  45672  cnrefiisplem  45827  dvnprodlem1  45944  dvnprodlem2  45945  fourierdlem80  46184  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0iunmpt  46416  iundjiun  46458  meaiininclem  46484  hoicvr  46546  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem3  46595  hspmbllem2  46625  opnvonmbllem2  46631  iunhoiioolem  46673  smfaddlem1  46761  smflimlem2  46770  smfmullem4  46792  smflimmpt  46808  smflimsuplem7  46824  smflimsuplem8  46825  smflimsupmpt  46827  smfliminfmpt  46830  fsupdm  46840  finfdm  46844  fsetsniunop  47050  otiunsndisjX  47280  iccpartiun  47435  stgredgiun  47957  iunord  49665