Theorem eliun 4950

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 3461	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3461	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3133	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2824	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3160	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4948	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3635	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  ∃wrex 3060  Vcvv 3440  ∪ ciun 4946

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-v 3442  df-iun 4948

This theorem is referenced by:  eliuni  4952  eliund  4953  iuncom  4954  iuncom4  4955  iunconst  4956  iuneqconst  4958  iuniin  4959  iinssiun  4960  iunss1  4961  ss2iun  4965  nfiu1  4982  iunssf  4998  iunss  5000  ssiun  5002  ssiun2  5003  iunab  5007  iun0  5017  0iun  5018  iunn0  5022  iunin2  5026  iundif2  5029  iindif2  5032  iunxsng  5045  iunxsngf  5047  iunun  5048  iunxun  5049  iunxdif3  5050  iunxiun  5052  iunpwss  5062  disjiun  5086  disjiund  5089  disjxiun  5095  triun  5219  otiunsndisj  5468  xpiundi  5695  xpiundir  5696  iunxpf  5797  cnvuni  5835  dmiun  5862  dmuni  5863  rniun  6105  xpdifid  6126  dfco2  6203  dfco2a  6204  coiun  6215  imaiun  7191  eluniima  7196  iunpw  7716  fiun  7887  f1iun  7888  opabex3d  7909  opabex3rd  7910  opabex3  7911  onoviun  8275  smoiun  8293  oalimcl  8487  oaass  8488  oarec  8489  omordlim  8504  omlimcl  8505  omeulem1  8509  oelimcl  8528  oeeulem  8529  oaabs2  8577  omabs  8579  dffi3  9334  ixpiunwdom  9495  ttrclselem2  9635  trcl  9637  r1ordg  9690  r1pwss  9696  rankr1ai  9710  r1elss  9718  fseqenlem2  9935  infpwfien  9972  cardaleph  9999  ackbij2  10152  cfsmolem  10180  alephsing  10186  hsmexlem2  10337  ac6c4  10391  ttukeylem6  10424  iunfo  10449  iundom2g  10450  konigthlem  10479  alephreg  10493  pwcfsdom  10494  pwfseqlem3  10571  inar1  10686  inatsk  10689  fsuppmapnn0fiub  13914  wrdval  14439  s3iunsndisj  14891  dfrtrclrec2  14981  fsum2dlem  15693  fsumcom2  15697  fsumiun  15744  fprod2dlem  15903  fprodcom2  15907  prmreclem5  16848  imasaddfnlem  17449  imasvscafn  17458  smndex1basss  18830  smndex1mgm  18832  smndex1mndlem  18834  smndex1n0mnd  18837  efgsfo  19668  frgpnabllem1  19802  lssats2  20951  lbsextlem2  21114  lbsextlem3  21115  islpidl  21280  pzriprnglem10  21445  pzriprnglem12  21447  pzriprnglem13  21448  pzriprnglem14  21449  iunocv  21636  iunconnlem  23371  iunconn  23372  locfincmp  23470  alexsubALTlem3  23993  ptcmplem3  23998  imasdsf1olem  24317  zcld  24758  ovolfioo  25424  ovolficc  25425  ovoliunlem2  25460  ovoliunnul  25464  volfiniun  25504  iundisj  25505  iunmbl2  25514  volsup2  25562  vitalilem2  25566  ismbf3d  25611  mbfaddlem  25617  mbfsup  25621  i1faddlem  25650  i1fmullem  25651  elaa  26280  oldlim  27883  precsexlem10  28212  precsexlem11  28213  numedglnl  29217  clwwlknun  30187  fusgreg2wsp  30411  iunin1f  32632  ssiun3  32633  iunpreima  32639  iundisjf  32664  unipreima  32721  aciunf1lem  32740  ofpreima  32743  iundisjfi  32876  fsumiunle  32910  gsumpart  33146  gsumwrd2dccatlem  33159  elirng  33843  irngnzply1  33848  irngnminplynz  33869  constrconj  33902  locfinreflem  33997  esum2dlem  34249  esum2d  34250  esumiun  34251  eulerpartlemgh  34535  dstfrvunirn  34632  reprsuc  34772  reprdifc  34784  bnj1405  34992  bnj916  35089  bnj983  35107  bnj1398  35190  bnj1417  35197  bnj1498  35217  fmlan0  35585  mclsppslem  35777  colinearex  36254  neibastop2lem  36554  weiunlem  36657  rdgellim  37581  exrecfnlem  37584  rabiun  37794  iundif1  37795  volsupnfl  37866  istotbnd3  37972  sstotbnd  37976  sstotbnd3  37977  prdstotbnd  37995  cntotbnd  37997  heiborlem3  38014  heibor  38022  pclfinN  40160  pclcmpatN  40161  lcfrvalsnN  41801  lcfrlem5  41806  lcfrlem6  41807  lcfrlem16  41818  lcfrlem27  41829  lcfrlem37  41839  lcfr  41845  mapdrvallem2  41905  grpods  42448  cnviun  43891  imaiun1  43892  coiun1  43893  ss2iundf  43900  eliunov2  43920  iunconnlem2  45175  iunincfi  45338  eliuniin  45343  eliuniin2  45364  eliunid  45391  iindif2f  45404  unirnmap  45452  unirnmapsn  45458  ssmapsn  45460  iunmapsn  45461  iuneqfzuzlem  45579  allbutfi  45637  fsumiunss  45821  fnlimfvre  45918  cnrefiisplem  46073  dvnprodlem1  46190  dvnprodlem2  46191  fourierdlem80  46430  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0iunmpt  46662  iundjiun  46704  meaiininclem  46730  hoicvr  46792  hoidmv1lelem3  46837  hoidmv1le  46838  hoidmvlelem3  46841  hspmbllem2  46871  opnvonmbllem2  46877  iunhoiioolem  46919  smfaddlem1  47007  smflimlem2  47016  smfmullem4  47038  smflimmpt  47054  smflimsuplem7  47070  smflimsuplem8  47071  smflimsupmpt  47073  smfliminfmpt  47076  fsupdm  47086  finfdm  47090  fsetsniunop  47295  otiunsndisjX  47525  iccpartiun  47680  stgredgiun  48204  iunord  49921