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 3475	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3475	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3163	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2852	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3190	. . 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 2147  ∃wrex 3090  Vcvv 3454  ∪ 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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  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  4989  iunssf  5004  iunss  5006  ssiun  5008  ssiun2  5009  iunab  5013  iun0  5023  0iun  5024  iunn0  5028  iunin2  5032  iundif2  5035  iindif2  5040  iunxsng  5053  iunxsngf  5055  iunun  5056  iunxun  5057  iunxdif3  5058  iunxiun  5060  iunpwss  5070  disjiun  5094  disjiund  5097  disjxiun  5103  triun  5230  otiunsndisj  5497  xpiundi  5726  xpiundir  5727  iunxpf  5832  cnvuni  5875  dmiun  5902  dmuni  5903  rniun  6151  xpdifid  6171  xpdifcnvepel  6172  dfco2  6259  dfco2a  6260  coiun  6271  iunpreima  7092  imaiun  7272  eluniima  7277  iunpw  7809  fiun  7979  f1iun  7980  opabex3d  8001  opabex3rd  8002  opabex3  8003  onoviun  8379  smoiun  8397  oalimcl  8596  oaass  8597  oarec  8598  omordlim  8613  omlimcl  8614  omeulem1  8618  oelimcl  8637  oeeulem  8638  oaabs2  8686  omabs  8688  dffi3  9450  ixpiunwdom  9611  ttrclselem2  9754  trcl  9756  r1ordg  9812  r1pwss  9818  rankr1ai  9833  r1elss  9841  fseqenlem2  10131  infpwfien  10168  cardaleph  10195  ackbij2  10347  cfsmolem  10375  alephsing  10381  hsmexlem2  10532  ttukeylem6  10619  iunfo  10650  iundom2g  10651  konigthlem  10680  alephreg  10694  pwcfsdom  10695  pwfseqlem3  10772  inar1  10887  inatsk  10890  fsuppmapnn0fiub  14161  wrdval  14688  s3iunsndisj  15150  dfrtrclrec2  15240  fsum2dlem  15965  fsumcom2  15969  fsumiun  16017  fprod2dlem  16176  fprodcom2  16180  prmreclem5  17127  imasaddfnlem  17729  imasvscafn  17738  smndex1basss  19133  smndex1mgm  19135  smndex1mndlem  19137  smndex1n0mnd  19140  efgsfo  19983  frgpnabllem1  20117  lssats2  21305  lbsextlem2  21467  lbsextlem3  21468  islpidl  21679  pzriprnglem10  21826  pzriprnglem12  21828  pzriprnglem13  21829  pzriprnglem14  21830  iunocv  22017  iunconnlem  23775  iunconn  23776  locfincmp  23875  alexsubALTlem3  24398  ptcmplem3  24403  imasdsf1olem  24722  zcld  25163  ovolfioo  25818  ovolficc  25819  ovoliunlem2  25854  ovoliunnul  25858  volfiniun  25898  iundisj  25899  iunmbl2  25908  volsup2  25956  vitalilem2  25960  ismbf3d  26005  mbfaddlem  26011  mbfsup  26015  i1faddlem  26044  i1fmullem  26045  elaa  26669  oldlim  28303  precsexlem10  28632  precsexlem11  28633  numedglnl  29752  clwwlknun  30733  fusgreg2wsp  30967  iunin1f  33224  ssiun3  33225  iundisjf  33255  unipreima  33309  aciunf1lem  33328  ofpreima  33331  iundisjfi  33458  fsumiunle  33490  gsumpart  33694  gsumwrd2dccatlem  33708  elirng  34388  irngnzply1  34393  irngnminplynz  34414  constrconj  34447  locfinreflem  34542  esum2dlem  34794  esum2d  34795  esumiun  34796  eulerpartlemgh  35080  dstfrvunirn  35177  reprsuc  35314  reprdifc  35326  bnj1405  35536  bnj916  35633  bnj983  35651  bnj1398  35734  bnj1417  35741  bnj1498  35761  fmlan0  36323  mclsppslem  36515  colinearex  37003  neibastop2lem  37326  weiunlem  37429  ttctr  37459  rdgellim  38491  exrecfnlem  38494  rabiun  38713  iundif1  38714  volsupnfl  38775  istotbnd3  38897  sstotbnd  38901  sstotbnd3  38902  prdstotbnd  38920  cntotbnd  38922  heiborlem3  38939  heibor  38947  pclfinN  41149  pclcmpatN  41150  lcfrvalsnN  42790  lcfrlem5  42795  lcfrlem6  42796  lcfrlem16  42807  lcfrlem27  42818  lcfrlem37  42828  lcfr  42834  mapdrvallem2  42894  grpods  43436  cnviun  44842  imaiun1  44843  coiun1  44844  ss2iundf  44851  eliunov2  44871  iunconnlem2  46108  iunincfi  46314  eliuniin  46319  eliuniin2  46340  eliunid  46367  iindif2f  46380  unirnmap  46426  unirnmapsn  46432  ssmapsn  46434  iunmapsn  46435  iuneqfzuzlem  46551  allbutfi  46609  fsumiunss  46792  fnlimfvre  46889  cnrefiisplem  47044  dvnprodlem1  47161  dvnprodlem2  47162  fourierdlem80  47401  sge0iunmptlemfi  47628  sge0iunmptlemre  47630  sge0iunmpt  47633  iundjiun  47675  meaiininclem  47701  hoidmv1lelem3  47808  hoidmv1le  47809  hoidmvlelem3  47812  hspmbllem2  47842  opnvonmbllem2  47848  iunhoiioolem  47890  smfaddlem1  47978  smflimlem2  47987  smfmullem4  48009  smflimmpt  48025  smflimsuplem7  48041  smflimsuplem8  48042  smflimsupmpt  48044  smfliminfmpt  48047  fsupdm  48057  finfdm  48061  fsetsniunop  48324  otiunsndisjX  48554  iccpartiun  48721  stgredgiun  49261  iunord  51064