Theorem eliun 4995

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 3501	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3501	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3151	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2829	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3179	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4993	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3680	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∃wrex 3070  Vcvv 3480  ∪ ciun 4991

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-v 3482  df-iun 4993

This theorem is referenced by:  eliuni  4997  eliund  4998  iuncom  4999  iuncom4  5000  iunconst  5001  iuneqconst  5003  iuniin  5004  iinssiun  5005  iunss1  5006  ss2iun  5010  nfiu1  5027  dfiun2gOLD  5031  ssiun  5046  ssiun2  5047  iunab  5051  iun0  5062  0iun  5063  iunn0  5067  iunin2  5071  iundif2  5074  iindif2  5077  iunxsng  5090  iunxsngf  5092  iunun  5093  iunxun  5094  iunxdif3  5095  iunxiun  5097  iunpwss  5107  disjiun  5131  disjiund  5134  disjxiun  5140  triun  5274  otiunsndisj  5525  xpiundi  5756  xpiundir  5757  iunxpf  5859  cnvuni  5897  dmiun  5924  dmuni  5925  rniun  6167  xpdifid  6188  dfco2  6265  dfco2a  6266  coiun  6276  imaiun  7265  eluniima  7270  iunpw  7791  fiun  7967  f1iun  7968  opabex3d  7990  opabex3rd  7991  opabex3  7992  wfrdmclOLD  8357  onoviun  8383  smoiun  8401  oalimcl  8598  oaass  8599  oarec  8600  omordlim  8615  omlimcl  8616  omeulem1  8620  oelimcl  8638  oeeulem  8639  oaabs2  8687  omabs  8689  dffi3  9471  ixpiunwdom  9630  ttrclselem2  9766  trcl  9768  r1ordg  9818  r1pwss  9824  rankr1ai  9838  r1elss  9846  fseqenlem2  10065  infpwfien  10102  cardaleph  10129  ackbij2  10282  cfsmolem  10310  alephsing  10316  hsmexlem2  10467  ac6c4  10521  ttukeylem6  10554  iunfo  10579  iundom2g  10580  konigthlem  10608  alephreg  10622  pwcfsdom  10623  pwfseqlem3  10700  inar1  10815  inatsk  10818  fsuppmapnn0fiub  14032  wrdval  14555  s3iunsndisj  15007  dfrtrclrec2  15097  fsum2dlem  15806  fsumcom2  15810  fsumiun  15857  fprod2dlem  16016  fprodcom2  16020  prmreclem5  16958  imasaddfnlem  17573  imasvscafn  17582  smndex1basss  18918  smndex1mgm  18920  smndex1mndlem  18922  smndex1n0mnd  18925  efgsfo  19757  frgpnabllem1  19891  lssats2  20998  lbsextlem2  21161  lbsextlem3  21162  islpidl  21335  pzriprnglem10  21501  pzriprnglem12  21503  pzriprnglem13  21504  pzriprnglem14  21505  iunocv  21699  iunconnlem  23435  iunconn  23436  locfincmp  23534  alexsubALTlem3  24057  ptcmplem3  24062  imasdsf1olem  24383  zcld  24835  ovolfioo  25502  ovolficc  25503  ovoliunlem2  25538  ovoliunnul  25542  volfiniun  25582  iundisj  25583  iunmbl2  25592  volsup2  25640  vitalilem2  25644  ismbf3d  25689  mbfaddlem  25695  mbfsup  25699  i1faddlem  25728  i1fmullem  25729  elaa  26358  oldlim  27925  precsexlem10  28240  precsexlem11  28241  numedglnl  29161  clwwlknun  30131  fusgreg2wsp  30355  iunin1f  32570  ssiun3  32571  iunpreima  32577  iundisjf  32602  unipreima  32653  aciunf1lem  32672  ofpreima  32675  iundisjfi  32798  fsumiunle  32831  gsumpart  33060  gsumwrd2dccatlem  33069  elirng  33736  irngnzply1  33741  irngnminplynz  33755  constrconj  33786  locfinreflem  33839  esum2dlem  34093  esum2d  34094  esumiun  34095  eulerpartlemgh  34380  dstfrvunirn  34477  reprsuc  34630  reprdifc  34642  bnj1405  34850  bnj916  34947  bnj983  34965  bnj1398  35048  bnj1417  35055  bnj1498  35075  fmlan0  35396  mclsppslem  35588  colinearex  36061  neibastop2lem  36361  weiunlem2  36464  rdgellim  37377  exrecfnlem  37380  rabiun  37600  iundif1  37601  volsupnfl  37672  istotbnd3  37778  sstotbnd  37782  sstotbnd3  37783  prdstotbnd  37801  cntotbnd  37803  heiborlem3  37820  heibor  37828  pclfinN  39902  pclcmpatN  39903  lcfrvalsnN  41543  lcfrlem5  41548  lcfrlem6  41549  lcfrlem16  41560  lcfrlem27  41571  lcfrlem37  41581  lcfr  41587  mapdrvallem2  41647  grpods  42195  cnviun  43663  imaiun1  43664  coiun1  43665  ss2iundf  43672  eliunov2  43692  iunconnlem2  44955  iunincfi  45099  eliuniin  45104  eliuniin2  45125  eliunid  45152  iindif2f  45165  unirnmap  45213  unirnmapsn  45219  ssmapsn  45221  iunmapsn  45222  iuneqfzuzlem  45345  allbutfi  45404  fsumiunss  45590  fnlimfvre  45689  cnrefiisplem  45844  dvnprodlem1  45961  dvnprodlem2  45962  fourierdlem80  46201  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0iunmpt  46433  iundjiun  46475  meaiininclem  46501  hoicvr  46563  hoidmv1lelem3  46608  hoidmv1le  46609  hoidmvlelem3  46612  hspmbllem2  46642  opnvonmbllem2  46648  iunhoiioolem  46690  smfaddlem1  46778  smflimlem2  46787  smfmullem4  46809  smflimmpt  46825  smflimsuplem7  46841  smflimsuplem8  46842  smflimsupmpt  46844  smfliminfmpt  46847  fsupdm  46857  finfdm  46861  fsetsniunop  47061  otiunsndisjX  47291  iccpartiun  47421  stgredgiun  47925  iunord  49195