Theorem eliun 4943

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 3455	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3455	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3127	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2817	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3154	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4941	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2110  ∃wrex 3054  Vcvv 3434  ∪ ciun 4939

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3436  df-iun 4941

This theorem is referenced by:  eliuni  4945  eliund  4946  iuncom  4947  iuncom4  4948  iunconst  4949  iuneqconst  4951  iuniin  4952  iinssiun  4953  iunss1  4954  ss2iun  4958  nfiu1  4975  ssiun  4993  ssiun2  4994  iunab  4998  iun0  5008  0iun  5009  iunn0  5013  iunin2  5017  iundif2  5020  iindif2  5023  iunxsng  5036  iunxsngf  5038  iunun  5039  iunxun  5040  iunxdif3  5041  iunxiun  5043  iunpwss  5053  disjiun  5077  disjiund  5080  disjxiun  5086  triun  5210  otiunsndisj  5458  xpiundi  5685  xpiundir  5686  iunxpf  5786  cnvuni  5824  dmiun  5851  dmuni  5852  rniun  6091  xpdifid  6112  dfco2  6189  dfco2a  6190  coiun  6200  imaiun  7174  eluniima  7179  iunpw  7699  fiun  7870  f1iun  7871  opabex3d  7892  opabex3rd  7893  opabex3  7894  onoviun  8258  smoiun  8276  oalimcl  8470  oaass  8471  oarec  8472  omordlim  8487  omlimcl  8488  omeulem1  8492  oelimcl  8510  oeeulem  8511  oaabs2  8559  omabs  8561  dffi3  9310  ixpiunwdom  9471  ttrclselem2  9611  trcl  9613  r1ordg  9663  r1pwss  9669  rankr1ai  9683  r1elss  9691  fseqenlem2  9908  infpwfien  9945  cardaleph  9972  ackbij2  10125  cfsmolem  10153  alephsing  10159  hsmexlem2  10310  ac6c4  10364  ttukeylem6  10397  iunfo  10422  iundom2g  10423  konigthlem  10451  alephreg  10465  pwcfsdom  10466  pwfseqlem3  10543  inar1  10658  inatsk  10661  fsuppmapnn0fiub  13890  wrdval  14415  s3iunsndisj  14867  dfrtrclrec2  14957  fsum2dlem  15669  fsumcom2  15673  fsumiun  15720  fprod2dlem  15879  fprodcom2  15883  prmreclem5  16824  imasaddfnlem  17424  imasvscafn  17433  smndex1basss  18805  smndex1mgm  18807  smndex1mndlem  18809  smndex1n0mnd  18812  efgsfo  19644  frgpnabllem1  19778  lssats2  20926  lbsextlem2  21089  lbsextlem3  21090  islpidl  21255  pzriprnglem10  21420  pzriprnglem12  21422  pzriprnglem13  21423  pzriprnglem14  21424  iunocv  21611  iunconnlem  23335  iunconn  23336  locfincmp  23434  alexsubALTlem3  23957  ptcmplem3  23962  imasdsf1olem  24281  zcld  24722  ovolfioo  25388  ovolficc  25389  ovoliunlem2  25424  ovoliunnul  25428  volfiniun  25468  iundisj  25469  iunmbl2  25478  volsup2  25526  vitalilem2  25530  ismbf3d  25575  mbfaddlem  25581  mbfsup  25585  i1faddlem  25614  i1fmullem  25615  elaa  26244  oldlim  27825  precsexlem10  28147  precsexlem11  28148  numedglnl  29115  clwwlknun  30082  fusgreg2wsp  30306  iunin1f  32527  ssiun3  32528  iunpreima  32534  iundisjf  32559  unipreima  32615  aciunf1lem  32634  ofpreima  32637  iundisjfi  32768  fsumiunle  32802  gsumpart  33027  gsumwrd2dccatlem  33036  elirng  33689  irngnzply1  33694  irngnminplynz  33715  constrconj  33748  locfinreflem  33843  esum2dlem  34095  esum2d  34096  esumiun  34097  eulerpartlemgh  34381  dstfrvunirn  34478  reprsuc  34618  reprdifc  34630  bnj1405  34838  bnj916  34935  bnj983  34953  bnj1398  35036  bnj1417  35043  bnj1498  35063  fmlan0  35403  mclsppslem  35595  colinearex  36073  neibastop2lem  36373  weiunlem2  36476  rdgellim  37389  exrecfnlem  37392  rabiun  37612  iundif1  37613  volsupnfl  37684  istotbnd3  37790  sstotbnd  37794  sstotbnd3  37795  prdstotbnd  37813  cntotbnd  37815  heiborlem3  37832  heibor  37840  pclfinN  39918  pclcmpatN  39919  lcfrvalsnN  41559  lcfrlem5  41564  lcfrlem6  41565  lcfrlem16  41576  lcfrlem27  41587  lcfrlem37  41597  lcfr  41603  mapdrvallem2  41663  grpods  42206  cnviun  43662  imaiun1  43663  coiun1  43664  ss2iundf  43671  eliunov2  43691  iunconnlem2  44946  iunincfi  45110  eliuniin  45115  eliuniin2  45136  eliunid  45163  iindif2f  45176  unirnmap  45224  unirnmapsn  45230  ssmapsn  45232  iunmapsn  45233  iuneqfzuzlem  45352  allbutfi  45410  fsumiunss  45594  fnlimfvre  45691  cnrefiisplem  45846  dvnprodlem1  45963  dvnprodlem2  45964  fourierdlem80  46203  sge0iunmptlemfi  46430  sge0iunmptlemre  46432  sge0iunmpt  46435  iundjiun  46477  meaiininclem  46503  hoicvr  46565  hoidmv1lelem3  46610  hoidmv1le  46611  hoidmvlelem3  46614  hspmbllem2  46644  opnvonmbllem2  46650  iunhoiioolem  46692  smfaddlem1  46780  smflimlem2  46789  smfmullem4  46811  smflimmpt  46827  smflimsuplem7  46843  smflimsuplem8  46844  smflimsupmpt  46846  smfliminfmpt  46849  fsupdm  46859  finfdm  46863  fsetsniunop  47059  otiunsndisjX  47289  iccpartiun  47444  stgredgiun  47968  iunord  49687