Theorem eliun 4929

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 3451	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3212	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2827	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3227	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4927	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3612	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2107  ∃wrex 3066  Vcvv 3433  ∪ ciun 4925

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3435  df-iun 4927

This theorem is referenced by:  eliuni  4931  iuncom  4932  iuncom4  4933  iunconst  4934  iuneqconst  4936  iuniin  4937  iinssiun  4938  iunss1  4939  ss2iun  4943  dfiun2gOLD  4962  ssiun  4977  ssiun2  4978  iunab  4982  iun0  4992  0iun  4993  iunn0  4997  iunin2  5001  iundif2  5004  iindif2  5007  iunxsng  5020  iunxsngf  5022  iunun  5023  iunxun  5024  iunxdif3  5025  iunxiun  5027  iunpwss  5037  disjiun  5062  disjiund  5065  disjxiun  5072  triun  5205  otiunsndisj  5435  xpiundi  5658  xpiundir  5659  iunxpf  5760  cnvuni  5798  dmiun  5825  dmuni  5826  rniun  6056  xpdifid  6076  dfco2  6153  dfco2a  6154  coiun  6164  imaiun  7127  eluniima  7132  iunpw  7630  fiun  7794  f1iun  7795  opabex3d  7817  opabex3rd  7818  opabex3  7819  wfrdmclOLD  8157  onoviun  8183  smoiun  8201  oalimcl  8400  oaass  8401  oarec  8402  omordlim  8417  omlimcl  8418  omeulem1  8422  oelimcl  8440  oeeulem  8441  oaabs2  8488  omabs  8490  dffi3  9199  ixpiunwdom  9358  ttrclselem2  9493  trcl  9495  r1ordg  9545  r1pwss  9551  rankr1ai  9565  r1elss  9573  fseqenlem2  9790  infpwfien  9827  cardaleph  9854  ackbij2  10008  cfsmolem  10035  alephsing  10041  hsmexlem2  10192  ac6c4  10246  ttukeylem6  10279  iunfo  10304  iundom2g  10305  konigthlem  10333  alephreg  10347  pwcfsdom  10348  pwfseqlem3  10425  inar1  10540  inatsk  10543  fsuppmapnn0fiub  13720  wrdval  14229  s3iunsndisj  14688  dfrtrclrec2  14778  fsum2dlem  15491  fsumcom2  15495  fsumiun  15542  fprod2dlem  15699  fprodcom2  15703  prmreclem5  16630  imasaddfnlem  17248  imasvscafn  17257  smndex1basss  18553  smndex1mgm  18555  smndex1mndlem  18557  smndex1n0mnd  18560  efgsfo  19354  frgpnabllem1  19483  lssats2  20271  lbsextlem2  20430  lbsextlem3  20431  islpidl  20526  iunocv  20895  iunconnlem  22587  iunconn  22588  locfincmp  22686  alexsubALTlem3  23209  ptcmplem3  23214  imasdsf1olem  23535  zcld  23985  ovolfioo  24640  ovolficc  24641  ovoliunlem2  24676  ovoliunnul  24680  volfiniun  24720  iundisj  24721  iunmbl2  24730  volsup2  24778  vitalilem2  24782  ismbf3d  24827  mbfaddlem  24833  mbfsup  24837  i1faddlem  24866  i1fmullem  24867  elaa  25485  numedglnl  27523  clwwlknun  28485  fusgreg2wsp  28709  iunin1f  30906  ssiun3  30907  iunpreima  30913  iundisjf  30937  unipreima  30990  aciunf1lem  31008  ofpreima  31011  iundisjfi  31126  fsumiunle  31152  gsumpart  31324  locfinreflem  31799  esum2dlem  32069  esum2d  32070  esumiun  32071  eulerpartlemgh  32354  dstfrvunirn  32450  reprsuc  32604  reprdifc  32616  bnj1405  32825  bnj916  32922  bnj983  32940  bnj1398  33023  bnj1417  33030  bnj1498  33050  fmlan0  33362  mclsppslem  33554  oldlim  34078  colinearex  34371  neibastop2lem  34558  rdgellim  35556  exrecfnlem  35559  rabiun  35759  iundif1  35760  volsupnfl  35831  istotbnd3  35938  sstotbnd  35942  sstotbnd3  35943  prdstotbnd  35961  cntotbnd  35963  heiborlem3  35980  heibor  35988  pclfinN  37921  pclcmpatN  37922  lcfrvalsnN  39562  lcfrlem5  39567  lcfrlem6  39568  lcfrlem16  39579  lcfrlem27  39590  lcfrlem37  39600  lcfr  39606  mapdrvallem2  39666  prjcrv0  40477  cnviun  41265  imaiun1  41266  coiun1  41267  ss2iundf  41274  eliunov2  41294  iunconnlem2  42562  iunincfi  42651  eliuniin  42656  eliuniin2  42676  eliunid  42706  unirnmap  42755  unirnmapsn  42761  ssmapsn  42763  iunmapsn  42764  iuneqfzuzlem  42880  allbutfi  42940  fsumiunss  43123  fnlimfvre  43222  cnrefiisplem  43377  dvnprodlem1  43494  dvnprodlem2  43495  fourierdlem80  43734  sge0iunmptlemfi  43958  sge0iunmptlemre  43960  sge0iunmpt  43963  iundjiun  44005  meaiininclem  44031  hoicvr  44093  hoidmv1lelem3  44138  hoidmv1le  44139  hoidmvlelem3  44142  hspmbllem2  44172  opnvonmbllem2  44178  iunhoiioolem  44220  smfaddlem1  44308  smflimlem2  44317  smfmullem4  44339  smflimmpt  44354  smflimsuplem7  44370  smflimsuplem8  44371  smflimsupmpt  44373  smfliminfmpt  44376  fsetsniunop  44554  otiunsndisjX  44782  iccpartiun  44897  iunord  46393