Theorem eliun 4954

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 3471	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3159	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2848	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3186	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4952	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 381	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144  ∃wrex 3086  Vcvv 3450  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-iun 4952

This theorem is used by:  eliuni  4956  eliund  4957  iuncom  4958  iuncom4  4959  iunconst  4960  iuneqconst  4962  iuniin  4963  iinssiun  4964  iunss1  4965  ss2iun  4969  nfiu1  4985  iunssf  5000  iunss  5002  ssiun  5004  ssiun2  5005  iunab  5009  iun0  5019  0iun  5020  iunn0  5024  iunin2  5028  iundif2  5031  iindif2  5036  iunxsng  5049  iunxsngf  5051  iunun  5052  iunxun  5053  iunxdif3  5054  iunxiun  5056  iunpwss  5066  disjiun  5090  disjiund  5093  disjxiun  5099  triun  5226  otiunsndisj  5492  xpiundi  5721  xpiundir  5722  iunxpf  5825  cnvuni  5867  dmiun  5894  dmuni  5895  rniun  6138  xpdifid  6158  xpdifcnvepel  6159  dfco2  6246  dfco2a  6247  coiun  6258  iunpreima  7068  imaiun  7249  eluniima  7254  iunpw  7785  fiun  7955  f1iun  7956  opabex3d  7977  opabex3rd  7978  opabex3  7979  onoviun  8351  smoiun  8369  oalimcl  8568  oaass  8569  oarec  8570  omordlim  8585  omlimcl  8586  omeulem1  8590  oelimcl  8609  oeeulem  8610  oaabs2  8658  omabs  8660  dffi3  9423  ixpiunwdom  9584  ttrclselem2  9727  trcl  9729  r1ordg  9785  r1pwss  9791  rankr1ai  9806  r1elss  9814  fseqenlem2  10104  infpwfien  10141  cardaleph  10168  ackbij2  10320  cfsmolem  10348  alephsing  10354  hsmexlem2  10505  ac6c4  10559  ttukeylem6  10592  iunfo  10623  iundom2g  10624  konigthlem  10653  alephreg  10667  pwcfsdom  10668  pwfseqlem3  10745  inar1  10860  inatsk  10863  fsuppmapnn0fiub  14134  wrdval  14661  s3iunsndisj  15121  dfrtrclrec2  15211  fsum2dlem  15936  fsumcom2  15940  fsumiun  15988  fprod2dlem  16147  fprodcom2  16151  prmreclem5  17098  imasaddfnlem  17700  imasvscafn  17709  smndex1basss  19104  smndex1mgm  19106  smndex1mndlem  19108  smndex1n0mnd  19111  efgsfo  19953  frgpnabllem1  20087  lssats2  21275  lbsextlem2  21437  lbsextlem3  21438  islpidl  21649  pzriprnglem10  21796  pzriprnglem12  21798  pzriprnglem13  21799  pzriprnglem14  21800  iunocv  21987  iunconnlem  23745  iunconn  23746  locfincmp  23845  alexsubALTlem3  24368  ptcmplem3  24373  imasdsf1olem  24692  zcld  25133  ovolfioo  25788  ovolficc  25789  ovoliunlem2  25824  ovoliunnul  25828  volfiniun  25868  iundisj  25869  iunmbl2  25878  volsup2  25926  vitalilem2  25930  ismbf3d  25975  mbfaddlem  25981  mbfsup  25985  i1faddlem  26014  i1fmullem  26015  elaa  26639  oldlim  28273  precsexlem10  28602  precsexlem11  28603  numedglnl  29722  clwwlknun  30703  fusgreg2wsp  30937  iunin1f  33194  ssiun3  33195  iundisjf  33225  unipreima  33279  aciunf1lem  33298  ofpreima  33301  iundisjfi  33430  fsumiunle  33462  gsumpart  33666  gsumwrd2dccatlem  33680  elirng  34360  irngnzply1  34365  irngnminplynz  34386  constrconj  34419  locfinreflem  34514  esum2dlem  34766  esum2d  34767  esumiun  34768  eulerpartlemgh  35052  dstfrvunirn  35149  reprsuc  35286  reprdifc  35298  bnj1405  35508  bnj916  35605  bnj983  35623  bnj1398  35706  bnj1417  35713  bnj1498  35733  fmlan0  36198  mclsppslem  36390  colinearex  36867  neibastop2lem  37190  weiunlem  37293  ttctr  37323  rdgellim  38342  exrecfnlem  38345  rabiun  38564  iundif1  38565  volsupnfl  38626  istotbnd3  38748  sstotbnd  38752  sstotbnd3  38753  prdstotbnd  38771  cntotbnd  38773  heiborlem3  38790  heibor  38798  pclfinN  41000  pclcmpatN  41001  lcfrvalsnN  42641  lcfrlem5  42646  lcfrlem6  42647  lcfrlem16  42658  lcfrlem27  42669  lcfrlem37  42679  lcfr  42685  mapdrvallem2  42745  grpods  43287  cnviun  44693  imaiun1  44694  coiun1  44695  ss2iundf  44702  eliunov2  44722  iunconnlem2  45960  iunincfi  46152  eliuniin  46157  eliuniin2  46178  eliunid  46205  iindif2f  46218  unirnmap  46264  unirnmapsn  46270  ssmapsn  46272  iunmapsn  46273  iuneqfzuzlem  46389  allbutfi  46447  fsumiunss  46630  fnlimfvre  46727  cnrefiisplem  46882  dvnprodlem1  46999  dvnprodlem2  47000  fourierdlem80  47239  sge0iunmptlemfi  47466  sge0iunmptlemre  47468  sge0iunmpt  47471  iundjiun  47513  meaiininclem  47539  hoidmv1lelem3  47646  hoidmv1le  47647  hoidmvlelem3  47650  hspmbllem2  47680  opnvonmbllem2  47686  iunhoiioolem  47728  smfaddlem1  47816  smflimlem2  47825  smfmullem4  47847  smflimmpt  47863  smflimsuplem7  47879  smflimsuplem8  47880  smflimsupmpt  47882  smfliminfmpt  47885  fsupdm  47895  finfdm  47899  fsetsniunop  48162  otiunsndisjX  48392  iccpartiun  48559  stgredgiun  49099  iunord  50827