Theorem eliun 4962

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3054  Vcvv 3450  ∪ ciun 4958

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-iun 4960

This theorem is referenced by:  eliuni  4964  eliund  4965  iuncom  4966  iuncom4  4967  iunconst  4968  iuneqconst  4970  iuniin  4971  iinssiun  4972  iunss1  4973  ss2iun  4977  nfiu1  4994  dfiun2gOLD  4998  ssiun  5013  ssiun2  5014  iunab  5018  iun0  5029  0iun  5030  iunn0  5034  iunin2  5038  iundif2  5041  iindif2  5044  iunxsng  5057  iunxsngf  5059  iunun  5060  iunxun  5061  iunxdif3  5062  iunxiun  5064  iunpwss  5074  disjiun  5098  disjiund  5101  disjxiun  5107  triun  5232  otiunsndisj  5483  xpiundi  5712  xpiundir  5713  iunxpf  5815  cnvuni  5853  dmiun  5880  dmuni  5881  rniun  6123  xpdifid  6144  dfco2  6221  dfco2a  6222  coiun  6232  imaiun  7222  eluniima  7227  iunpw  7750  fiun  7924  f1iun  7925  opabex3d  7947  opabex3rd  7948  opabex3  7949  onoviun  8315  smoiun  8333  oalimcl  8527  oaass  8528  oarec  8529  omordlim  8544  omlimcl  8545  omeulem1  8549  oelimcl  8567  oeeulem  8568  oaabs2  8616  omabs  8618  dffi3  9389  ixpiunwdom  9550  ttrclselem2  9686  trcl  9688  r1ordg  9738  r1pwss  9744  rankr1ai  9758  r1elss  9766  fseqenlem2  9985  infpwfien  10022  cardaleph  10049  ackbij2  10202  cfsmolem  10230  alephsing  10236  hsmexlem2  10387  ac6c4  10441  ttukeylem6  10474  iunfo  10499  iundom2g  10500  konigthlem  10528  alephreg  10542  pwcfsdom  10543  pwfseqlem3  10620  inar1  10735  inatsk  10738  fsuppmapnn0fiub  13963  wrdval  14488  s3iunsndisj  14941  dfrtrclrec2  15031  fsum2dlem  15743  fsumcom2  15747  fsumiun  15794  fprod2dlem  15953  fprodcom2  15957  prmreclem5  16898  imasaddfnlem  17498  imasvscafn  17507  smndex1basss  18839  smndex1mgm  18841  smndex1mndlem  18843  smndex1n0mnd  18846  efgsfo  19676  frgpnabllem1  19810  lssats2  20913  lbsextlem2  21076  lbsextlem3  21077  islpidl  21242  pzriprnglem10  21407  pzriprnglem12  21409  pzriprnglem13  21410  pzriprnglem14  21411  iunocv  21597  iunconnlem  23321  iunconn  23322  locfincmp  23420  alexsubALTlem3  23943  ptcmplem3  23948  imasdsf1olem  24268  zcld  24709  ovolfioo  25375  ovolficc  25376  ovoliunlem2  25411  ovoliunnul  25415  volfiniun  25455  iundisj  25456  iunmbl2  25465  volsup2  25513  vitalilem2  25517  ismbf3d  25562  mbfaddlem  25568  mbfsup  25572  i1faddlem  25601  i1fmullem  25602  elaa  26231  oldlim  27805  precsexlem10  28125  precsexlem11  28126  numedglnl  29078  clwwlknun  30048  fusgreg2wsp  30272  iunin1f  32493  ssiun3  32494  iunpreima  32500  iundisjf  32525  unipreima  32574  aciunf1lem  32593  ofpreima  32596  iundisjfi  32726  fsumiunle  32761  gsumpart  33004  gsumwrd2dccatlem  33013  elirng  33688  irngnzply1  33693  irngnminplynz  33709  constrconj  33742  locfinreflem  33837  esum2dlem  34089  esum2d  34090  esumiun  34091  eulerpartlemgh  34376  dstfrvunirn  34473  reprsuc  34613  reprdifc  34625  bnj1405  34833  bnj916  34930  bnj983  34948  bnj1398  35031  bnj1417  35038  bnj1498  35058  fmlan0  35385  mclsppslem  35577  colinearex  36055  neibastop2lem  36355  weiunlem2  36458  rdgellim  37371  exrecfnlem  37374  rabiun  37594  iundif1  37595  volsupnfl  37666  istotbnd3  37772  sstotbnd  37776  sstotbnd3  37777  prdstotbnd  37795  cntotbnd  37797  heiborlem3  37814  heibor  37822  pclfinN  39901  pclcmpatN  39902  lcfrvalsnN  41542  lcfrlem5  41547  lcfrlem6  41548  lcfrlem16  41559  lcfrlem27  41570  lcfrlem37  41580  lcfr  41586  mapdrvallem2  41646  grpods  42189  cnviun  43646  imaiun1  43647  coiun1  43648  ss2iundf  43655  eliunov2  43675  iunconnlem2  44931  iunincfi  45095  eliuniin  45100  eliuniin2  45121  eliunid  45148  iindif2f  45161  unirnmap  45209  unirnmapsn  45215  ssmapsn  45217  iunmapsn  45218  iuneqfzuzlem  45337  allbutfi  45396  fsumiunss  45580  fnlimfvre  45679  cnrefiisplem  45834  dvnprodlem1  45951  dvnprodlem2  45952  fourierdlem80  46191  sge0iunmptlemfi  46418  sge0iunmptlemre  46420  sge0iunmpt  46423  iundjiun  46465  meaiininclem  46491  hoicvr  46553  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem3  46602  hspmbllem2  46632  opnvonmbllem2  46638  iunhoiioolem  46680  smfaddlem1  46768  smflimlem2  46777  smfmullem4  46799  smflimmpt  46815  smflimsuplem7  46831  smflimsuplem8  46832  smflimsupmpt  46834  smfliminfmpt  46837  fsupdm  46847  finfdm  46851  fsetsniunop  47054  otiunsndisjX  47284  iccpartiun  47439  stgredgiun  47961  iunord  49669