Theorem eliun 4971

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 3480	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3480	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3137	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2822	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3164	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4969	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3659	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  ∃wrex 3060  Vcvv 3459  ∪ ciun 4967

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-iun 4969

This theorem is referenced by:  eliuni  4973  eliund  4974  iuncom  4975  iuncom4  4976  iunconst  4977  iuneqconst  4979  iuniin  4980  iinssiun  4981  iunss1  4982  ss2iun  4986  nfiu1  5003  dfiun2gOLD  5007  ssiun  5022  ssiun2  5023  iunab  5027  iun0  5038  0iun  5039  iunn0  5043  iunin2  5047  iundif2  5050  iindif2  5053  iunxsng  5066  iunxsngf  5068  iunun  5069  iunxun  5070  iunxdif3  5071  iunxiun  5073  iunpwss  5083  disjiun  5107  disjiund  5110  disjxiun  5116  triun  5244  otiunsndisj  5495  xpiundi  5725  xpiundir  5726  iunxpf  5828  cnvuni  5866  dmiun  5893  dmuni  5894  rniun  6136  xpdifid  6157  dfco2  6234  dfco2a  6235  coiun  6245  imaiun  7236  eluniima  7241  iunpw  7763  fiun  7939  f1iun  7940  opabex3d  7962  opabex3rd  7963  opabex3  7964  wfrdmclOLD  8329  onoviun  8355  smoiun  8373  oalimcl  8570  oaass  8571  oarec  8572  omordlim  8587  omlimcl  8588  omeulem1  8592  oelimcl  8610  oeeulem  8611  oaabs2  8659  omabs  8661  dffi3  9441  ixpiunwdom  9602  ttrclselem2  9738  trcl  9740  r1ordg  9790  r1pwss  9796  rankr1ai  9810  r1elss  9818  fseqenlem2  10037  infpwfien  10074  cardaleph  10101  ackbij2  10254  cfsmolem  10282  alephsing  10288  hsmexlem2  10439  ac6c4  10493  ttukeylem6  10526  iunfo  10551  iundom2g  10552  konigthlem  10580  alephreg  10594  pwcfsdom  10595  pwfseqlem3  10672  inar1  10787  inatsk  10790  fsuppmapnn0fiub  14007  wrdval  14532  s3iunsndisj  14985  dfrtrclrec2  15075  fsum2dlem  15784  fsumcom2  15788  fsumiun  15835  fprod2dlem  15994  fprodcom2  15998  prmreclem5  16938  imasaddfnlem  17540  imasvscafn  17549  smndex1basss  18881  smndex1mgm  18883  smndex1mndlem  18885  smndex1n0mnd  18888  efgsfo  19718  frgpnabllem1  19852  lssats2  20955  lbsextlem2  21118  lbsextlem3  21119  islpidl  21284  pzriprnglem10  21449  pzriprnglem12  21451  pzriprnglem13  21452  pzriprnglem14  21453  iunocv  21639  iunconnlem  23363  iunconn  23364  locfincmp  23462  alexsubALTlem3  23985  ptcmplem3  23990  imasdsf1olem  24310  zcld  24751  ovolfioo  25418  ovolficc  25419  ovoliunlem2  25454  ovoliunnul  25458  volfiniun  25498  iundisj  25499  iunmbl2  25508  volsup2  25556  vitalilem2  25560  ismbf3d  25605  mbfaddlem  25611  mbfsup  25615  i1faddlem  25644  i1fmullem  25645  elaa  26274  oldlim  27842  precsexlem10  28157  precsexlem11  28158  numedglnl  29069  clwwlknun  30039  fusgreg2wsp  30263  iunin1f  32484  ssiun3  32485  iunpreima  32491  iundisjf  32516  unipreima  32567  aciunf1lem  32586  ofpreima  32589  iundisjfi  32719  fsumiunle  32754  gsumpart  32997  gsumwrd2dccatlem  33006  elirng  33673  irngnzply1  33678  irngnminplynz  33692  constrconj  33725  locfinreflem  33817  esum2dlem  34069  esum2d  34070  esumiun  34071  eulerpartlemgh  34356  dstfrvunirn  34453  reprsuc  34593  reprdifc  34605  bnj1405  34813  bnj916  34910  bnj983  34928  bnj1398  35011  bnj1417  35018  bnj1498  35038  fmlan0  35359  mclsppslem  35551  colinearex  36024  neibastop2lem  36324  weiunlem2  36427  rdgellim  37340  exrecfnlem  37343  rabiun  37563  iundif1  37564  volsupnfl  37635  istotbnd3  37741  sstotbnd  37745  sstotbnd3  37746  prdstotbnd  37764  cntotbnd  37766  heiborlem3  37783  heibor  37791  pclfinN  39865  pclcmpatN  39866  lcfrvalsnN  41506  lcfrlem5  41511  lcfrlem6  41512  lcfrlem16  41523  lcfrlem27  41534  lcfrlem37  41544  lcfr  41550  mapdrvallem2  41610  grpods  42153  cnviun  43621  imaiun1  43622  coiun1  43623  ss2iundf  43630  eliunov2  43650  iunconnlem2  44907  iunincfi  45066  eliuniin  45071  eliuniin2  45092  eliunid  45119  iindif2f  45132  unirnmap  45180  unirnmapsn  45186  ssmapsn  45188  iunmapsn  45189  iuneqfzuzlem  45309  allbutfi  45368  fsumiunss  45552  fnlimfvre  45651  cnrefiisplem  45806  dvnprodlem1  45923  dvnprodlem2  45924  fourierdlem80  46163  sge0iunmptlemfi  46390  sge0iunmptlemre  46392  sge0iunmpt  46395  iundjiun  46437  meaiininclem  46463  hoicvr  46525  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem3  46574  hspmbllem2  46604  opnvonmbllem2  46610  iunhoiioolem  46652  smfaddlem1  46740  smflimlem2  46749  smfmullem4  46771  smflimmpt  46787  smflimsuplem7  46803  smflimsuplem8  46804  smflimsupmpt  46806  smfliminfmpt  46809  fsupdm  46819  finfdm  46823  fsetsniunop  47026  otiunsndisjX  47256  iccpartiun  47396  stgredgiun  47918  iunord  49488