Theorem eliun 4958

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3088  Vcvv 3453  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3455  df-iun 4956

This theorem is used by:  eliuni  4960  eliund  4961  iuncom  4962  iuncom4  4963  iunconst  4964  iuneqconst  4966  iuniin  4967  iinssiun  4968  iunss1  4969  ss2iun  4973  nfiu1  4990  iunssf  5005  iunss  5007  ssiun  5009  ssiun2  5010  iunab  5014  iun0  5024  0iun  5025  iunn0  5029  iunin2  5033  iundif2  5036  iindif2  5041  iunxsng  5054  iunxsngf  5056  iunun  5057  iunxun  5058  iunxdif3  5059  iunxiun  5061  iunpwss  5071  disjiun  5095  disjiund  5098  disjxiun  5104  triun  5231  otiunsndisj  5501  xpiundi  5730  xpiundir  5731  iunxpf  5832  cnvuni  5874  dmiun  5901  dmuni  5902  rniun  6143  xpdifid  6164  xpdifcnvepel  6165  dfco2  6245  dfco2a  6246  coiun  6257  imaiun  7245  eluniima  7250  iunpw  7773  fiun  7943  f1iun  7944  opabex3d  7965  opabex3rd  7966  opabex3  7967  onoviun  8335  smoiun  8353  oalimcl  8550  oaass  8551  oarec  8552  omordlim  8567  omlimcl  8568  omeulem1  8572  oelimcl  8591  oeeulem  8592  oaabs2  8640  omabs  8642  dffi3  9404  ixpiunwdom  9565  ttrclselem2  9708  trcl  9710  r1ordg  9763  r1pwss  9769  rankr1ai  9783  r1elss  9791  fseqenlem2  10031  infpwfien  10068  cardaleph  10095  ackbij2  10247  cfsmolem  10275  alephsing  10281  hsmexlem2  10432  ac6c4  10486  ttukeylem6  10519  iunfo  10550  iundom2g  10551  konigthlem  10580  alephreg  10594  pwcfsdom  10595  pwfseqlem3  10672  inar1  10787  inatsk  10790  fsuppmapnn0fiub  14057  wrdval  14583  s3iunsndisj  15043  dfrtrclrec2  15133  fsum2dlem  15858  fsumcom2  15862  fsumiun  15910  fprod2dlem  16071  fprodcom2  16075  prmreclem5  17016  imasaddfnlem  17618  imasvscafn  17627  smndex1basss  19018  smndex1mgm  19020  smndex1mndlem  19022  smndex1n0mnd  19025  efgsfo  19867  frgpnabllem1  20001  lssats2  21185  lbsextlem2  21347  lbsextlem3  21348  islpidl  21557  pzriprnglem10  21704  pzriprnglem12  21706  pzriprnglem13  21707  pzriprnglem14  21708  iunocv  21895  iunconnlem  23653  iunconn  23654  locfincmp  23753  alexsubALTlem3  24276  ptcmplem3  24281  imasdsf1olem  24600  zcld  25041  ovolfioo  25696  ovolficc  25697  ovoliunlem2  25732  ovoliunnul  25736  volfiniun  25776  iundisj  25777  iunmbl2  25786  volsup2  25834  vitalilem2  25838  ismbf3d  25883  mbfaddlem  25889  mbfsup  25893  i1faddlem  25922  i1fmullem  25923  elaa  26547  oldlim  28150  precsexlem10  28479  precsexlem11  28480  numedglnl  29587  clwwlknun  30568  fusgreg2wsp  30802  iunin1f  33017  ssiun3  33018  iunpreima  33024  iundisjf  33049  unipreima  33103  aciunf1lem  33122  ofpreima  33125  iundisjfi  33254  fsumiunle  33286  gsumpart  33490  gsumwrd2dccatlem  33504  elirng  34183  irngnzply1  34188  irngnminplynz  34209  constrconj  34242  locfinreflem  34337  esum2dlem  34589  esum2d  34590  esumiun  34591  eulerpartlemgh  34876  dstfrvunirn  34973  reprsuc  35110  reprdifc  35122  bnj1405  35332  bnj916  35429  bnj983  35447  bnj1398  35530  bnj1417  35537  bnj1498  35557  fmlan0  35957  mclsppslem  36149  colinearex  36627  neibastop2lem  36966  weiunlem  37069  ttctr  37099  rdgellim  38117  exrecfnlem  38120  rabiun  38339  iundif1  38340  volsupnfl  38401  istotbnd3  38508  sstotbnd  38512  sstotbnd3  38513  prdstotbnd  38531  cntotbnd  38533  heiborlem3  38550  heibor  38558  pclfinN  40760  pclcmpatN  40761  lcfrvalsnN  42401  lcfrlem5  42406  lcfrlem6  42407  lcfrlem16  42418  lcfrlem27  42429  lcfrlem37  42439  lcfr  42445  mapdrvallem2  42505  grpods  43047  cnviun  44477  imaiun1  44478  coiun1  44479  ss2iundf  44486  eliunov2  44506  iunconnlem2  45744  iunincfi  45913  eliuniin  45918  eliuniin2  45939  eliunid  45966  iindif2f  45979  unirnmap  46025  unirnmapsn  46031  ssmapsn  46033  iunmapsn  46034  iuneqfzuzlem  46151  allbutfi  46209  fsumiunss  46392  fnlimfvre  46489  cnrefiisplem  46644  dvnprodlem1  46761  dvnprodlem2  46762  fourierdlem80  47001  sge0iunmptlemfi  47228  sge0iunmptlemre  47230  sge0iunmpt  47233  iundjiun  47275  meaiininclem  47301  hoidmv1lelem3  47408  hoidmv1le  47409  hoidmvlelem3  47412  hspmbllem2  47442  opnvonmbllem2  47448  iunhoiioolem  47490  smfaddlem1  47578  smflimlem2  47587  smfmullem4  47609  smflimmpt  47625  smflimsuplem7  47641  smflimsuplem8  47642  smflimsupmpt  47644  smfliminfmpt  47647  fsupdm  47657  finfdm  47661  fsetsniunop  47924  otiunsndisjX  48154  iccpartiun  48321  stgredgiun  48861  iunord  50589