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  7193  eluniima  7198  iunpw  7718  fiun  7889  f1iun  7890  opabex3d  7911  opabex3rd  7912  opabex3  7913  onoviun  8277  smoiun  8295  oalimcl  8489  oaass  8490  oarec  8491  omordlim  8506  omlimcl  8507  omeulem1  8511  oelimcl  8530  oeeulem  8531  oaabs2  8579  omabs  8581  dffi3  9338  ixpiunwdom  9499  ttrclselem2  9639  trcl  9641  r1ordg  9694  r1pwss  9700  rankr1ai  9714  r1elss  9722  fseqenlem2  9939  infpwfien  9976  cardaleph  10003  ackbij2  10156  cfsmolem  10184  alephsing  10190  hsmexlem2  10341  ac6c4  10395  ttukeylem6  10428  iunfo  10453  iundom2g  10454  konigthlem  10483  alephreg  10497  pwcfsdom  10498  pwfseqlem3  10575  inar1  10690  inatsk  10693  fsuppmapnn0fiub  13918  wrdval  14443  s3iunsndisj  14895  dfrtrclrec2  14985  fsum2dlem  15697  fsumcom2  15701  fsumiun  15748  fprod2dlem  15907  fprodcom2  15911  prmreclem5  16852  imasaddfnlem  17453  imasvscafn  17462  smndex1basss  18834  smndex1mgm  18836  smndex1mndlem  18838  smndex1n0mnd  18841  efgsfo  19672  frgpnabllem1  19806  lssats2  20955  lbsextlem2  21118  lbsextlem3  21119  islpidl  21284  pzriprnglem10  21449  pzriprnglem12  21451  pzriprnglem13  21452  pzriprnglem14  21453  iunocv  21640  iunconnlem  23375  iunconn  23376  locfincmp  23474  alexsubALTlem3  23997  ptcmplem3  24002  imasdsf1olem  24321  zcld  24762  ovolfioo  25428  ovolficc  25429  ovoliunlem2  25464  ovoliunnul  25468  volfiniun  25508  iundisj  25509  iunmbl2  25518  volsup2  25566  vitalilem2  25570  ismbf3d  25615  mbfaddlem  25621  mbfsup  25625  i1faddlem  25654  i1fmullem  25655  elaa  26284  oldlim  27869  precsexlem10  28197  precsexlem11  28198  numedglnl  29200  clwwlknun  30170  fusgreg2wsp  30394  iunin1f  32614  ssiun3  32615  iunpreima  32621  iundisjf  32646  unipreima  32703  aciunf1lem  32722  ofpreima  32725  iundisjfi  32857  fsumiunle  32891  gsumpart  33127  gsumwrd2dccatlem  33140  elirng  33824  irngnzply1  33829  irngnminplynz  33850  constrconj  33883  locfinreflem  33978  esum2dlem  34230  esum2d  34231  esumiun  34232  eulerpartlemgh  34516  dstfrvunirn  34613  reprsuc  34753  reprdifc  34765  bnj1405  34973  bnj916  35070  bnj983  35088  bnj1398  35171  bnj1417  35178  bnj1498  35198  fmlan0  35566  mclsppslem  35758  colinearex  36235  neibastop2lem  36535  weiunlem2  36638  rdgellim  37552  exrecfnlem  37555  rabiun  37765  iundif1  37766  volsupnfl  37837  istotbnd3  37943  sstotbnd  37947  sstotbnd3  37948  prdstotbnd  37966  cntotbnd  37968  heiborlem3  37985  heibor  37993  pclfinN  40197  pclcmpatN  40198  lcfrvalsnN  41838  lcfrlem5  41843  lcfrlem6  41844  lcfrlem16  41855  lcfrlem27  41866  lcfrlem37  41876  lcfr  41882  mapdrvallem2  41942  grpods  42485  cnviun  43927  imaiun1  43928  coiun1  43929  ss2iundf  43936  eliunov2  43956  iunconnlem2  45211  iunincfi  45374  eliuniin  45379  eliuniin2  45400  eliunid  45427  iindif2f  45440  unirnmap  45488  unirnmapsn  45494  ssmapsn  45496  iunmapsn  45497  iuneqfzuzlem  45615  allbutfi  45673  fsumiunss  45857  fnlimfvre  45954  cnrefiisplem  46109  dvnprodlem1  46226  dvnprodlem2  46227  fourierdlem80  46466  sge0iunmptlemfi  46693  sge0iunmptlemre  46695  sge0iunmpt  46698  iundjiun  46740  meaiininclem  46766  hoicvr  46828  hoidmv1lelem3  46873  hoidmv1le  46874  hoidmvlelem3  46877  hspmbllem2  46907  opnvonmbllem2  46913  iunhoiioolem  46955  smfaddlem1  47043  smflimlem2  47052  smfmullem4  47074  smflimmpt  47090  smflimsuplem7  47106  smflimsuplem8  47107  smflimsupmpt  47109  smfliminfmpt  47112  fsupdm  47122  finfdm  47126  fsetsniunop  47331  otiunsndisjX  47561  iccpartiun  47716  stgredgiun  48240  iunord  49957