Theorem eliun 4947

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 3459	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3131	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2821	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3158	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4945	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3058  Vcvv 3438  ∪ ciun 4943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rex 3059  df-v 3440  df-iun 4945

This theorem is referenced by:  eliuni  4949  eliund  4950  iuncom  4951  iuncom4  4952  iunconst  4953  iuneqconst  4955  iuniin  4956  iinssiun  4957  iunss1  4958  ss2iun  4962  nfiu1  4979  iunssf  4995  iunss  4997  ssiun  4999  ssiun2  5000  iunab  5004  iun0  5014  0iun  5015  iunn0  5019  iunin2  5023  iundif2  5026  iindif2  5029  iunxsng  5042  iunxsngf  5044  iunun  5045  iunxun  5046  iunxdif3  5047  iunxiun  5049  iunpwss  5059  disjiun  5083  disjiund  5086  disjxiun  5092  triun  5216  otiunsndisj  5465  xpiundi  5692  xpiundir  5693  iunxpf  5795  cnvuni  5833  dmiun  5860  dmuni  5861  rniun  6102  xpdifid  6123  dfco2  6200  dfco2a  6201  coiun  6212  imaiun  7188  eluniima  7193  iunpw  7713  fiun  7884  f1iun  7885  opabex3d  7906  opabex3rd  7907  opabex3  7908  onoviun  8272  smoiun  8290  oalimcl  8484  oaass  8485  oarec  8486  omordlim  8501  omlimcl  8502  omeulem1  8506  oelimcl  8524  oeeulem  8525  oaabs2  8573  omabs  8575  dffi3  9325  ixpiunwdom  9486  ttrclselem2  9626  trcl  9628  r1ordg  9681  r1pwss  9687  rankr1ai  9701  r1elss  9709  fseqenlem2  9926  infpwfien  9963  cardaleph  9990  ackbij2  10143  cfsmolem  10171  alephsing  10177  hsmexlem2  10328  ac6c4  10382  ttukeylem6  10415  iunfo  10440  iundom2g  10441  konigthlem  10469  alephreg  10483  pwcfsdom  10484  pwfseqlem3  10561  inar1  10676  inatsk  10679  fsuppmapnn0fiub  13908  wrdval  14433  s3iunsndisj  14885  dfrtrclrec2  14975  fsum2dlem  15687  fsumcom2  15691  fsumiun  15738  fprod2dlem  15897  fprodcom2  15901  prmreclem5  16842  imasaddfnlem  17442  imasvscafn  17451  smndex1basss  18823  smndex1mgm  18825  smndex1mndlem  18827  smndex1n0mnd  18830  efgsfo  19661  frgpnabllem1  19795  lssats2  20943  lbsextlem2  21106  lbsextlem3  21107  islpidl  21272  pzriprnglem10  21437  pzriprnglem12  21439  pzriprnglem13  21440  pzriprnglem14  21441  iunocv  21628  iunconnlem  23352  iunconn  23353  locfincmp  23451  alexsubALTlem3  23974  ptcmplem3  23979  imasdsf1olem  24298  zcld  24739  ovolfioo  25405  ovolficc  25406  ovoliunlem2  25441  ovoliunnul  25445  volfiniun  25485  iundisj  25486  iunmbl2  25495  volsup2  25543  vitalilem2  25547  ismbf3d  25592  mbfaddlem  25598  mbfsup  25602  i1faddlem  25631  i1fmullem  25632  elaa  26261  oldlim  27842  precsexlem10  28164  precsexlem11  28165  numedglnl  29133  clwwlknun  30103  fusgreg2wsp  30327  iunin1f  32548  ssiun3  32549  iunpreima  32555  iundisjf  32580  unipreima  32636  aciunf1lem  32655  ofpreima  32658  iundisjfi  32789  fsumiunle  32823  gsumpart  33048  gsumwrd2dccatlem  33057  elirng  33710  irngnzply1  33715  irngnminplynz  33736  constrconj  33769  locfinreflem  33864  esum2dlem  34116  esum2d  34117  esumiun  34118  eulerpartlemgh  34402  dstfrvunirn  34499  reprsuc  34639  reprdifc  34651  bnj1405  34859  bnj916  34956  bnj983  34974  bnj1398  35057  bnj1417  35064  bnj1498  35084  fmlan0  35446  mclsppslem  35638  colinearex  36115  neibastop2lem  36415  weiunlem2  36518  rdgellim  37431  exrecfnlem  37434  rabiun  37643  iundif1  37644  volsupnfl  37715  istotbnd3  37821  sstotbnd  37825  sstotbnd3  37826  prdstotbnd  37844  cntotbnd  37846  heiborlem3  37863  heibor  37871  pclfinN  40009  pclcmpatN  40010  lcfrvalsnN  41650  lcfrlem5  41655  lcfrlem6  41656  lcfrlem16  41667  lcfrlem27  41678  lcfrlem37  41688  lcfr  41694  mapdrvallem2  41754  grpods  42297  cnviun  43757  imaiun1  43758  coiun1  43759  ss2iundf  43766  eliunov2  43786  iunconnlem2  45041  iunincfi  45205  eliuniin  45210  eliuniin2  45231  eliunid  45258  iindif2f  45271  unirnmap  45319  unirnmapsn  45325  ssmapsn  45327  iunmapsn  45328  iuneqfzuzlem  45447  allbutfi  45505  fsumiunss  45689  fnlimfvre  45786  cnrefiisplem  45941  dvnprodlem1  46058  dvnprodlem2  46059  fourierdlem80  46298  sge0iunmptlemfi  46525  sge0iunmptlemre  46527  sge0iunmpt  46530  iundjiun  46572  meaiininclem  46598  hoicvr  46660  hoidmv1lelem3  46705  hoidmv1le  46706  hoidmvlelem3  46709  hspmbllem2  46739  opnvonmbllem2  46745  iunhoiioolem  46787  smfaddlem1  46875  smflimlem2  46884  smfmullem4  46906  smflimmpt  46922  smflimsuplem7  46938  smflimsuplem8  46939  smflimsupmpt  46941  smfliminfmpt  46944  fsupdm  46954  finfdm  46958  fsetsniunop  47163  otiunsndisjX  47393  iccpartiun  47548  stgredgiun  48072  iunord  49791