Theorem eliun 4938

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 3451	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3451	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3135	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2825	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3162	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4936	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3624	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062  Vcvv 3430  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3432  df-iun 4936

This theorem is referenced by:  eliuni  4940  eliund  4941  iuncom  4942  iuncom4  4943  iunconst  4944  iuneqconst  4946  iuniin  4947  iinssiun  4948  iunss1  4949  ss2iun  4953  nfiu1  4970  iunssf  4986  iunss  4988  ssiun  4990  ssiun2  4991  iunab  4995  iun0  5005  0iun  5006  iunn0  5010  iunin2  5014  iundif2  5017  iindif2  5020  iunxsng  5033  iunxsngf  5035  iunun  5036  iunxun  5037  iunxdif3  5038  iunxiun  5040  iunpwss  5050  disjiun  5074  disjiund  5077  disjxiun  5083  triun  5207  otiunsndisj  5466  xpiundi  5693  xpiundir  5694  iunxpf  5795  cnvuni  5833  dmiun  5860  dmuni  5861  rniun  6103  xpdifid  6124  dfco2  6201  dfco2a  6202  coiun  6213  imaiun  7191  eluniima  7196  iunpw  7716  fiun  7887  f1iun  7888  opabex3d  7909  opabex3rd  7910  opabex3  7911  onoviun  8274  smoiun  8292  oalimcl  8486  oaass  8487  oarec  8488  omordlim  8503  omlimcl  8504  omeulem1  8508  oelimcl  8527  oeeulem  8528  oaabs2  8576  omabs  8578  dffi3  9335  ixpiunwdom  9496  ttrclselem2  9636  trcl  9638  r1ordg  9691  r1pwss  9697  rankr1ai  9711  r1elss  9719  fseqenlem2  9936  infpwfien  9973  cardaleph  10000  ackbij2  10153  cfsmolem  10181  alephsing  10187  hsmexlem2  10338  ac6c4  10392  ttukeylem6  10425  iunfo  10450  iundom2g  10451  konigthlem  10480  alephreg  10494  pwcfsdom  10495  pwfseqlem3  10572  inar1  10687  inatsk  10690  fsuppmapnn0fiub  13915  wrdval  14440  s3iunsndisj  14892  dfrtrclrec2  14982  fsum2dlem  15694  fsumcom2  15698  fsumiun  15745  fprod2dlem  15904  fprodcom2  15908  prmreclem5  16849  imasaddfnlem  17450  imasvscafn  17459  smndex1basss  18834  smndex1mgm  18836  smndex1mndlem  18838  smndex1n0mnd  18841  efgsfo  19672  frgpnabllem1  19806  lssats2  20953  lbsextlem2  21116  lbsextlem3  21117  islpidl  21282  pzriprnglem10  21447  pzriprnglem12  21449  pzriprnglem13  21450  pzriprnglem14  21451  iunocv  21638  iunconnlem  23370  iunconn  23371  locfincmp  23469  alexsubALTlem3  23992  ptcmplem3  23997  imasdsf1olem  24316  zcld  24757  ovolfioo  25412  ovolficc  25413  ovoliunlem2  25448  ovoliunnul  25452  volfiniun  25492  iundisj  25493  iunmbl2  25502  volsup2  25550  vitalilem2  25554  ismbf3d  25599  mbfaddlem  25605  mbfsup  25609  i1faddlem  25638  i1fmullem  25639  elaa  26264  oldlim  27867  precsexlem10  28196  precsexlem11  28197  numedglnl  29201  clwwlknun  30171  fusgreg2wsp  30395  iunin1f  32616  ssiun3  32617  iunpreima  32623  iundisjf  32648  unipreima  32705  aciunf1lem  32724  ofpreima  32727  iundisjfi  32859  fsumiunle  32893  gsumpart  33129  gsumwrd2dccatlem  33143  elirng  33836  irngnzply1  33841  irngnminplynz  33862  constrconj  33895  locfinreflem  33990  esum2dlem  34242  esum2d  34243  esumiun  34244  eulerpartlemgh  34528  dstfrvunirn  34625  reprsuc  34765  reprdifc  34777  bnj1405  34984  bnj916  35081  bnj983  35099  bnj1398  35182  bnj1417  35189  bnj1498  35209  fmlan0  35579  mclsppslem  35771  colinearex  36248  neibastop2lem  36548  weiunlem  36651  ttctr  36681  rdgellim  37688  exrecfnlem  37691  rabiun  37905  iundif1  37906  volsupnfl  37977  istotbnd3  38083  sstotbnd  38087  sstotbnd3  38088  prdstotbnd  38106  cntotbnd  38108  heiborlem3  38125  heibor  38133  pclfinN  40337  pclcmpatN  40338  lcfrvalsnN  41978  lcfrlem5  41983  lcfrlem6  41984  lcfrlem16  41995  lcfrlem27  42006  lcfrlem37  42016  lcfr  42022  mapdrvallem2  42082  grpods  42625  cnviun  44080  imaiun1  44081  coiun1  44082  ss2iundf  44089  eliunov2  44109  iunconnlem2  45364  iunincfi  45527  eliuniin  45532  eliuniin2  45553  eliunid  45580  iindif2f  45593  unirnmap  45640  unirnmapsn  45646  ssmapsn  45648  iunmapsn  45649  iuneqfzuzlem  45767  allbutfi  45825  fsumiunss  46009  fnlimfvre  46106  cnrefiisplem  46261  dvnprodlem1  46378  dvnprodlem2  46379  fourierdlem80  46618  sge0iunmptlemfi  46845  sge0iunmptlemre  46847  sge0iunmpt  46850  iundjiun  46892  meaiininclem  46918  hoidmv1lelem3  47025  hoidmv1le  47026  hoidmvlelem3  47029  hspmbllem2  47059  opnvonmbllem2  47065  iunhoiioolem  47107  smfaddlem1  47195  smflimlem2  47204  smfmullem4  47226  smflimmpt  47242  smflimsuplem7  47258  smflimsuplem8  47259  smflimsupmpt  47261  smfliminfmpt  47264  fsupdm  47274  finfdm  47278  fsetsniunop  47483  otiunsndisjX  47713  iccpartiun  47868  stgredgiun  48392  iunord  50109