Theorem eliun 4951

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3061  Vcvv 3441  ∪ ciun 4947

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 3062  df-v 3443  df-iun 4949

This theorem is referenced by:  eliuni  4953  eliund  4954  iuncom  4955  iuncom4  4956  iunconst  4957  iuneqconst  4959  iuniin  4960  iinssiun  4961  iunss1  4962  ss2iun  4966  nfiu1  4983  iunssf  4999  iunss  5001  ssiun  5003  ssiun2  5004  iunab  5008  iun0  5018  0iun  5019  iunn0  5023  iunin2  5027  iundif2  5030  iindif2  5033  iunxsng  5046  iunxsngf  5048  iunun  5049  iunxun  5050  iunxdif3  5051  iunxiun  5053  iunpwss  5063  disjiun  5087  disjiund  5090  disjxiun  5096  triun  5220  otiunsndisj  5469  xpiundi  5696  xpiundir  5697  iunxpf  5798  cnvuni  5836  dmiun  5863  dmuni  5864  rniun  6106  xpdifid  6127  dfco2  6204  dfco2a  6205  coiun  6216  imaiun  7194  eluniima  7199  iunpw  7719  fiun  7890  f1iun  7891  opabex3d  7912  opabex3rd  7913  opabex3  7914  onoviun  8278  smoiun  8296  oalimcl  8490  oaass  8491  oarec  8492  omordlim  8507  omlimcl  8508  omeulem1  8512  oelimcl  8531  oeeulem  8532  oaabs2  8580  omabs  8582  dffi3  9339  ixpiunwdom  9500  ttrclselem2  9640  trcl  9642  r1ordg  9695  r1pwss  9701  rankr1ai  9715  r1elss  9723  fseqenlem2  9940  infpwfien  9977  cardaleph  10004  ackbij2  10157  cfsmolem  10185  alephsing  10191  hsmexlem2  10342  ac6c4  10396  ttukeylem6  10429  iunfo  10454  iundom2g  10455  konigthlem  10484  alephreg  10498  pwcfsdom  10499  pwfseqlem3  10576  inar1  10691  inatsk  10694  fsuppmapnn0fiub  13919  wrdval  14444  s3iunsndisj  14896  dfrtrclrec2  14986  fsum2dlem  15698  fsumcom2  15702  fsumiun  15749  fprod2dlem  15908  fprodcom2  15912  prmreclem5  16853  imasaddfnlem  17454  imasvscafn  17463  smndex1basss  18835  smndex1mgm  18837  smndex1mndlem  18839  smndex1n0mnd  18842  efgsfo  19673  frgpnabllem1  19807  lssats2  20956  lbsextlem2  21119  lbsextlem3  21120  islpidl  21285  pzriprnglem10  21450  pzriprnglem12  21452  pzriprnglem13  21453  pzriprnglem14  21454  iunocv  21641  iunconnlem  23376  iunconn  23377  locfincmp  23475  alexsubALTlem3  23998  ptcmplem3  24003  imasdsf1olem  24322  zcld  24763  ovolfioo  25429  ovolficc  25430  ovoliunlem2  25465  ovoliunnul  25469  volfiniun  25509  iundisj  25510  iunmbl2  25519  volsup2  25567  vitalilem2  25571  ismbf3d  25616  mbfaddlem  25622  mbfsup  25626  i1faddlem  25655  i1fmullem  25656  elaa  26285  oldlim  27888  precsexlem10  28217  precsexlem11  28218  numedglnl  29222  clwwlknun  30192  fusgreg2wsp  30416  iunin1f  32636  ssiun3  32637  iunpreima  32643  iundisjf  32668  unipreima  32725  aciunf1lem  32744  ofpreima  32747  iundisjfi  32879  fsumiunle  32913  gsumpart  33149  gsumwrd2dccatlem  33163  elirng  33856  irngnzply1  33861  irngnminplynz  33882  constrconj  33915  locfinreflem  34010  esum2dlem  34262  esum2d  34263  esumiun  34264  eulerpartlemgh  34548  dstfrvunirn  34645  reprsuc  34785  reprdifc  34797  bnj1405  35005  bnj916  35102  bnj983  35120  bnj1398  35203  bnj1417  35210  bnj1498  35230  fmlan0  35598  mclsppslem  35790  colinearex  36267  neibastop2lem  36567  weiunlem  36670  rdgellim  37594  exrecfnlem  37597  rabiun  37807  iundif1  37808  volsupnfl  37879  istotbnd3  37985  sstotbnd  37989  sstotbnd3  37990  prdstotbnd  38008  cntotbnd  38010  heiborlem3  38027  heibor  38035  pclfinN  40239  pclcmpatN  40240  lcfrvalsnN  41880  lcfrlem5  41885  lcfrlem6  41886  lcfrlem16  41897  lcfrlem27  41908  lcfrlem37  41918  lcfr  41924  mapdrvallem2  41984  grpods  42527  cnviun  43969  imaiun1  43970  coiun1  43971  ss2iundf  43978  eliunov2  43998  iunconnlem2  45253  iunincfi  45416  eliuniin  45421  eliuniin2  45442  eliunid  45469  iindif2f  45482  unirnmap  45529  unirnmapsn  45535  ssmapsn  45537  iunmapsn  45538  iuneqfzuzlem  45656  allbutfi  45714  fsumiunss  45898  fnlimfvre  45995  cnrefiisplem  46150  dvnprodlem1  46267  dvnprodlem2  46268  fourierdlem80  46507  sge0iunmptlemfi  46734  sge0iunmptlemre  46736  sge0iunmpt  46739  iundjiun  46781  meaiininclem  46807  hoicvr  46869  hoidmv1lelem3  46914  hoidmv1le  46915  hoidmvlelem3  46918  hspmbllem2  46948  opnvonmbllem2  46954  iunhoiioolem  46996  smfaddlem1  47084  smflimlem2  47093  smfmullem4  47115  smflimmpt  47131  smflimsuplem7  47147  smflimsuplem8  47148  smflimsupmpt  47150  smfliminfmpt  47153  fsupdm  47163  finfdm  47167  fsetsniunop  47372  otiunsndisjX  47602  iccpartiun  47757  stgredgiun  48281  iunord  49998