Theorem eliun 4923

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 3512	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3512	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3282	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2900	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3297	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4921	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3668	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 382	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  ∃wrex 3139  Vcvv 3494  ∪ ciun 4919

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-iun 4921

This theorem is referenced by:  eliuni  4925  iuncom  4926  iuncom4  4927  iunconst  4928  iuneqconst  4930  iuniin  4931  iinssiun  4932  iunss1  4933  ss2iun  4937  dfiun2g  4955  dfiun2gOLD  4956  ssiun  4970  ssiun2  4971  iunab  4975  iun0  4985  0iun  4986  iunn0  4989  iunin2  4993  iundif2  4996  iindif2  4999  iunxsng  5012  iunxsngf  5014  iunun  5015  iunxun  5016  iunxdif3  5017  iunxiun  5019  iunpwss  5029  disjiun  5053  disjiund  5056  disjxiun  5063  triun  5185  otiunsndisj  5410  xpiundi  5622  xpiundir  5623  iunxpf  5719  cnvuni  5757  dmiun  5782  dmuni  5783  rniun  6006  xpdifid  6025  dfco2  6098  dfco2a  6099  coiun  6109  imaiun  7004  eluniima  7009  iunpw  7493  fiun  7644  f1iun  7645  opabex3d  7666  opabex3rd  7667  opabex3  7668  wfrdmcl  7963  onoviun  7980  smoiun  7998  oalimcl  8186  oaass  8187  oarec  8188  omordlim  8203  omlimcl  8204  omeulem1  8208  oelimcl  8226  oeeulem  8227  oaabs2  8272  omabs  8274  dffi3  8895  ixpiunwdom  9055  trcl  9170  r1ordg  9207  r1pwss  9213  rankr1ai  9227  r1elss  9235  fseqenlem2  9451  infpwfien  9488  cardaleph  9515  ackbij2  9665  cfsmolem  9692  alephsing  9698  hsmexlem2  9849  ac6c4  9903  ttukeylem6  9936  iunfo  9961  iundom2g  9962  konigthlem  9990  alephreg  10004  pwcfsdom  10005  pwfseqlem3  10082  inar1  10197  inatsk  10200  fsuppmapnn0fiub  13360  wrdval  13865  s3iunsndisj  14328  dfrtrclrec2  14416  fsum2dlem  15125  fsumcom2  15129  fsumiun  15176  fprod2dlem  15334  fprodcom2  15338  prmreclem5  16256  imasaddfnlem  16801  imasvscafn  16810  smndex1basss  18070  smndex1mgm  18072  smndex1mndlem  18074  smndex1n0mnd  18077  efgsfo  18865  frgpnabllem1  18993  lssats2  19772  lbsextlem2  19931  lbsextlem3  19932  islpidl  20019  iunocv  20825  iunconnlem  22035  iunconn  22036  locfincmp  22134  alexsubALTlem3  22657  ptcmplem3  22662  imasdsf1olem  22983  zcld  23421  ovolfioo  24068  ovolficc  24069  ovoliunlem2  24104  ovoliunnul  24108  volfiniun  24148  iundisj  24149  iunmbl2  24158  volsup2  24206  vitalilem2  24210  ismbf3d  24255  mbfaddlem  24261  mbfsup  24265  i1faddlem  24294  i1fmullem  24295  elaa  24905  numedglnl  26929  clwwlknun  27891  fusgreg2wsp  28115  iunin1f  30309  ssiun3  30310  iunpreima  30316  iundisjf  30339  unipreima  30391  aciunf1lem  30407  ofpreima  30410  iundisjfi  30519  fsumiunle  30545  locfinreflem  31104  esum2dlem  31351  esum2d  31352  esumiun  31353  eulerpartlemgh  31636  dstfrvunirn  31732  reprsuc  31886  reprdifc  31898  bnj1405  32108  bnj916  32205  bnj983  32223  bnj1398  32306  bnj1417  32313  bnj1498  32333  fmlan0  32638  mclsppslem  32830  eltrpred  33065  dftrpred3g  33072  trpredrec  33077  colinearex  33521  neibastop2lem  33708  rdgellim  34660  exrecfnlem  34663  rabiun  34880  iundif1  34881  volsupnfl  34952  istotbnd3  35064  sstotbnd  35068  sstotbnd3  35069  prdstotbnd  35087  cntotbnd  35089  heiborlem3  35106  heibor  35114  pclfinN  37051  pclcmpatN  37052  lcfrvalsnN  38692  lcfrlem5  38697  lcfrlem6  38698  lcfrlem16  38709  lcfrlem27  38720  lcfrlem37  38730  lcfr  38736  mapdrvallem2  38796  cnviun  40015  imaiun1  40016  coiun1  40017  ss2iundf  40024  eliunov2  40044  iunconnlem2  41289  iunincfi  41380  eliuniin  41385  eliuniin2  41406  eliunid  41439  unirnmap  41491  unirnmapsn  41497  ssmapsn  41499  iunmapsn  41500  iuneqfzuzlem  41622  allbutfi  41685  fsumiunss  41876  fnlimfvre  41975  cnrefiisplem  42130  dvnprodlem1  42251  dvnprodlem2  42252  fourierdlem80  42491  sge0iunmptlemfi  42715  sge0iunmptlemre  42717  sge0iunmpt  42720  iundjiun  42762  meaiininclem  42788  hoicvr  42850  hoidmv1lelem3  42895  hoidmv1le  42896  hoidmvlelem3  42899  hspmbllem2  42929  opnvonmbllem2  42935  iunhoiioolem  42977  smfaddlem1  43059  smflimlem2  43068  smfmullem4  43089  smflimmpt  43104  smflimsuplem7  43120  smflimsuplem8  43121  smflimsupmpt  43123  smfliminfmpt  43126  otiunsndisjX  43498  iccpartiun  43614  iunord  44799