Theorem eliun 5002

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 3493	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3493	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3152	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2822	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3179	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 5000	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3671	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  ∃wrex 3071  Vcvv 3475  ∪ ciun 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rex 3072  df-v 3477  df-iun 5000

This theorem is referenced by:  eliuni  5004  iuncom  5005  iuncom4  5006  iunconst  5007  iuneqconst  5009  iuniin  5010  iinssiun  5011  iunss1  5012  ss2iun  5016  dfiun2gOLD  5035  ssiun  5050  ssiun2  5051  iunab  5055  iun0  5066  0iun  5067  iunn0  5071  iunin2  5075  iundif2  5078  iindif2  5081  iunxsng  5094  iunxsngf  5096  iunun  5097  iunxun  5098  iunxdif3  5099  iunxiun  5101  iunpwss  5111  disjiun  5136  disjiund  5139  disjxiun  5146  triun  5281  otiunsndisj  5521  xpiundi  5747  xpiundir  5748  iunxpf  5849  cnvuni  5887  dmiun  5914  dmuni  5915  rniun  6148  xpdifid  6168  dfco2  6245  dfco2a  6246  coiun  6256  imaiun  7244  eluniima  7249  iunpw  7758  fiun  7929  f1iun  7930  opabex3d  7952  opabex3rd  7953  opabex3  7954  wfrdmclOLD  8317  onoviun  8343  smoiun  8361  oalimcl  8560  oaass  8561  oarec  8562  omordlim  8577  omlimcl  8578  omeulem1  8582  oelimcl  8600  oeeulem  8601  oaabs2  8648  omabs  8650  dffi3  9426  ixpiunwdom  9585  ttrclselem2  9721  trcl  9723  r1ordg  9773  r1pwss  9779  rankr1ai  9793  r1elss  9801  fseqenlem2  10020  infpwfien  10057  cardaleph  10084  ackbij2  10238  cfsmolem  10265  alephsing  10271  hsmexlem2  10422  ac6c4  10476  ttukeylem6  10509  iunfo  10534  iundom2g  10535  konigthlem  10563  alephreg  10577  pwcfsdom  10578  pwfseqlem3  10655  inar1  10770  inatsk  10773  fsuppmapnn0fiub  13956  wrdval  14467  s3iunsndisj  14915  dfrtrclrec2  15005  fsum2dlem  15716  fsumcom2  15720  fsumiun  15767  fprod2dlem  15924  fprodcom2  15928  prmreclem5  16853  imasaddfnlem  17474  imasvscafn  17483  smndex1basss  18786  smndex1mgm  18788  smndex1mndlem  18790  smndex1n0mnd  18793  efgsfo  19607  frgpnabllem1  19741  lssats2  20611  lbsextlem2  20772  lbsextlem3  20773  islpidl  20884  iunocv  21234  iunconnlem  22931  iunconn  22932  locfincmp  23030  alexsubALTlem3  23553  ptcmplem3  23558  imasdsf1olem  23879  zcld  24329  ovolfioo  24984  ovolficc  24985  ovoliunlem2  25020  ovoliunnul  25024  volfiniun  25064  iundisj  25065  iunmbl2  25074  volsup2  25122  vitalilem2  25126  ismbf3d  25171  mbfaddlem  25177  mbfsup  25181  i1faddlem  25210  i1fmullem  25211  elaa  25829  oldlim  27381  precsexlem10  27662  precsexlem11  27663  numedglnl  28404  clwwlknun  29365  fusgreg2wsp  29589  iunin1f  31789  ssiun3  31790  iunpreima  31796  iundisjf  31820  unipreima  31869  aciunf1lem  31887  ofpreima  31890  iundisjfi  32007  fsumiunle  32035  gsumpart  32207  elirng  32750  irngnzply1  32755  irngnminplynz  32771  locfinreflem  32820  esum2dlem  33090  esum2d  33091  esumiun  33092  eulerpartlemgh  33377  dstfrvunirn  33473  reprsuc  33627  reprdifc  33639  bnj1405  33847  bnj916  33944  bnj983  33962  bnj1398  34045  bnj1417  34052  bnj1498  34072  fmlan0  34382  mclsppslem  34574  colinearex  35032  neibastop2lem  35245  rdgellim  36257  exrecfnlem  36260  rabiun  36461  iundif1  36462  volsupnfl  36533  istotbnd3  36639  sstotbnd  36643  sstotbnd3  36644  prdstotbnd  36662  cntotbnd  36664  heiborlem3  36681  heibor  36689  pclfinN  38771  pclcmpatN  38772  lcfrvalsnN  40412  lcfrlem5  40417  lcfrlem6  40418  lcfrlem16  40429  lcfrlem27  40440  lcfrlem37  40450  lcfr  40456  mapdrvallem2  40516  cnviun  42401  imaiun1  42402  coiun1  42403  ss2iundf  42410  eliunov2  42430  iunconnlem2  43696  iunincfi  43783  eliuniin  43788  eliuniin2  43809  eliunid  43839  iindif2f  43854  eliund  43857  unirnmap  43907  unirnmapsn  43913  ssmapsn  43915  iunmapsn  43916  iuneqfzuzlem  44044  allbutfi  44103  fsumiunss  44291  fnlimfvre  44390  cnrefiisplem  44545  dvnprodlem1  44662  dvnprodlem2  44663  fourierdlem80  44902  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0iunmpt  45134  iundjiun  45176  meaiininclem  45202  hoicvr  45264  hoidmv1lelem3  45309  hoidmv1le  45310  hoidmvlelem3  45313  hspmbllem2  45343  opnvonmbllem2  45349  iunhoiioolem  45391  smfaddlem1  45479  smflimlem2  45488  smfmullem4  45510  smflimmpt  45526  smflimsuplem7  45542  smflimsuplem8  45543  smflimsupmpt  45545  smfliminfmpt  45548  fsupdm  45558  finfdm  45562  fsetsniunop  45759  otiunsndisjX  45987  iccpartiun  46102  pzriprnglem10  46814  pzriprnglem12  46816  pzriprnglem13  46817  pzriprnglem14  46818  iunord  47721