Theorem eliun 4927

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 3448	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3448	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3132	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2823	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3159	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4925	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3620	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3059  Vcvv 3427  ∪ ciun 4923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-rex 3060  df-v 3429  df-iun 4925

This theorem is referenced by:  eliuni  4929  eliund  4930  iuncom  4931  iuncom4  4932  iunconst  4933  iuneqconst  4935  iuniin  4936  iinssiun  4937  iunss1  4938  ss2iun  4942  nfiu1  4959  iunssf  4974  iunss  4976  ssiun  4978  ssiun2  4979  iunab  4983  iun0  4993  0iun  4994  iunn0  4998  iunin2  5002  iundif2  5005  iindif2  5008  iunxsng  5021  iunxsngf  5023  iunun  5024  iunxun  5025  iunxdif3  5026  iunxiun  5028  iunpwss  5038  disjiun  5062  disjiund  5065  disjxiun  5071  triun  5196  otiunsndisj  5463  xpiundi  5691  xpiundir  5692  iunxpf  5792  cnvuni  5830  dmiun  5857  dmuni  5858  rniun  6100  xpdifid  6121  dfco2  6198  dfco2a  6199  coiun  6210  imaiun  7189  eluniima  7194  iunpw  7714  fiun  7885  f1iun  7886  opabex3d  7907  opabex3rd  7908  opabex3  7909  onoviun  8272  smoiun  8290  oalimcl  8484  oaass  8485  oarec  8486  omordlim  8501  omlimcl  8502  omeulem1  8506  oelimcl  8525  oeeulem  8526  oaabs2  8574  omabs  8576  dffi3  9333  ixpiunwdom  9494  ttrclselem2  9636  trcl  9638  r1ordg  9691  r1pwss  9697  rankr1ai  9711  r1elss  9719  fseqenlem2  9936  infpwfien  9973  cardaleph  10000  ackbij2  10153  cfsmolem  10181  alephsing  10187  hsmexlem2  10338  ac6c4  10392  ttukeylem6  10425  iunfo  10450  iundom2g  10451  konigthlem  10480  alephreg  10494  pwcfsdom  10495  pwfseqlem3  10572  inar1  10687  inatsk  10690  fsuppmapnn0fiub  13942  wrdval  14467  s3iunsndisj  14919  dfrtrclrec2  15009  fsum2dlem  15721  fsumcom2  15725  fsumiun  15773  fprod2dlem  15934  fprodcom2  15938  prmreclem5  16880  imasaddfnlem  17481  imasvscafn  17490  smndex1basss  18865  smndex1mgm  18867  smndex1mndlem  18869  smndex1n0mnd  18872  efgsfo  19703  frgpnabllem1  19837  lssats2  20984  lbsextlem2  21146  lbsextlem3  21147  islpidl  21312  pzriprnglem10  21459  pzriprnglem12  21461  pzriprnglem13  21462  pzriprnglem14  21463  iunocv  21650  iunconnlem  23380  iunconn  23381  locfincmp  23479  alexsubALTlem3  24002  ptcmplem3  24007  imasdsf1olem  24326  zcld  24767  ovolfioo  25422  ovolficc  25423  ovoliunlem2  25458  ovoliunnul  25462  volfiniun  25502  iundisj  25503  iunmbl2  25512  volsup2  25560  vitalilem2  25564  ismbf3d  25609  mbfaddlem  25615  mbfsup  25619  i1faddlem  25648  i1fmullem  25649  elaa  26270  oldlim  27867  precsexlem10  28196  precsexlem11  28197  numedglnl  29201  clwwlknun  30170  fusgreg2wsp  30394  iunin1f  32615  ssiun3  32616  iunpreima  32622  iundisjf  32647  unipreima  32704  aciunf1lem  32723  ofpreima  32726  iundisjfi  32857  fsumiunle  32890  gsumpart  33112  gsumwrd2dccatlem  33126  elirng  33818  irngnzply1  33823  irngnminplynz  33844  constrconj  33877  locfinreflem  33972  esum2dlem  34224  esum2d  34225  esumiun  34226  eulerpartlemgh  34510  dstfrvunirn  34607  reprsuc  34747  reprdifc  34759  bnj1405  34966  bnj916  35063  bnj983  35081  bnj1398  35164  bnj1417  35171  bnj1498  35191  fmlan0  35561  mclsppslem  35753  colinearex  36230  neibastop2lem  36530  weiunlem  36633  ttctr  36663  rdgellim  37680  exrecfnlem  37683  rabiun  37902  iundif1  37903  volsupnfl  37974  istotbnd3  38080  sstotbnd  38084  sstotbnd3  38085  prdstotbnd  38103  cntotbnd  38105  heiborlem3  38122  heibor  38130  pclfinN  40334  pclcmpatN  40335  lcfrvalsnN  41975  lcfrlem5  41980  lcfrlem6  41981  lcfrlem16  41992  lcfrlem27  42003  lcfrlem37  42013  lcfr  42019  mapdrvallem2  42079  grpods  42621  cnviun  44065  imaiun1  44066  coiun1  44067  ss2iundf  44074  eliunov2  44094  iunconnlem2  45349  iunincfi  45512  eliuniin  45517  eliuniin2  45538  eliunid  45565  iindif2f  45578  unirnmap  45625  unirnmapsn  45631  ssmapsn  45633  iunmapsn  45634  iuneqfzuzlem  45752  allbutfi  45810  fsumiunss  45993  fnlimfvre  46090  cnrefiisplem  46245  dvnprodlem1  46362  dvnprodlem2  46363  fourierdlem80  46602  sge0iunmptlemfi  46829  sge0iunmptlemre  46831  sge0iunmpt  46834  iundjiun  46876  meaiininclem  46902  hoidmv1lelem3  47009  hoidmv1le  47010  hoidmvlelem3  47013  hspmbllem2  47043  opnvonmbllem2  47049  iunhoiioolem  47091  smfaddlem1  47179  smflimlem2  47188  smfmullem4  47210  smflimmpt  47226  smflimsuplem7  47242  smflimsuplem8  47243  smflimsupmpt  47245  smfliminfmpt  47248  fsupdm  47258  finfdm  47262  fsetsniunop  47485  otiunsndisjX  47715  iccpartiun  47882  stgredgiun  48422  iunord  50139