Theorem eliun 4925

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 3440	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3440	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3210	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2826	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3225	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4923	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3604	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 379	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108  ∃wrex 3064  Vcvv 3422  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-iun 4923

This theorem is referenced by:  eliuni  4927  iuncom  4928  iuncom4  4929  iunconst  4930  iuneqconst  4932  iuniin  4933  iinssiun  4934  iunss1  4935  ss2iun  4939  dfiun2g  4957  ssiun  4972  ssiun2  4973  iunab  4977  iun0  4987  0iun  4988  iunn0  4992  iunin2  4996  iundif2  4999  iindif2  5002  iunxsng  5015  iunxsngf  5017  iunun  5018  iunxun  5019  iunxdif3  5020  iunxiun  5022  iunpwss  5032  disjiun  5057  disjiund  5060  disjxiun  5067  triun  5200  otiunsndisj  5428  xpiundi  5648  xpiundir  5649  iunxpf  5746  cnvuni  5784  dmiun  5811  dmuni  5812  rniun  6040  xpdifid  6060  dfco2  6138  dfco2a  6139  coiun  6149  imaiun  7100  eluniima  7105  iunpw  7599  fiun  7759  f1iun  7760  opabex3d  7781  opabex3rd  7782  opabex3  7783  wfrdmclOLD  8119  onoviun  8145  smoiun  8163  oalimcl  8353  oaass  8354  oarec  8355  omordlim  8370  omlimcl  8371  omeulem1  8375  oelimcl  8393  oeeulem  8394  oaabs2  8439  omabs  8441  dffi3  9120  ixpiunwdom  9279  eltrpred  9404  dftrpred3g  9412  trpredrec  9415  trcl  9417  r1ordg  9467  r1pwss  9473  rankr1ai  9487  r1elss  9495  fseqenlem2  9712  infpwfien  9749  cardaleph  9776  ackbij2  9930  cfsmolem  9957  alephsing  9963  hsmexlem2  10114  ac6c4  10168  ttukeylem6  10201  iunfo  10226  iundom2g  10227  konigthlem  10255  alephreg  10269  pwcfsdom  10270  pwfseqlem3  10347  inar1  10462  inatsk  10465  fsuppmapnn0fiub  13639  wrdval  14148  s3iunsndisj  14607  dfrtrclrec2  14697  fsum2dlem  15410  fsumcom2  15414  fsumiun  15461  fprod2dlem  15618  fprodcom2  15622  prmreclem5  16549  imasaddfnlem  17156  imasvscafn  17165  smndex1basss  18459  smndex1mgm  18461  smndex1mndlem  18463  smndex1n0mnd  18466  efgsfo  19260  frgpnabllem1  19389  lssats2  20177  lbsextlem2  20336  lbsextlem3  20337  islpidl  20430  iunocv  20798  iunconnlem  22486  iunconn  22487  locfincmp  22585  alexsubALTlem3  23108  ptcmplem3  23113  imasdsf1olem  23434  zcld  23882  ovolfioo  24536  ovolficc  24537  ovoliunlem2  24572  ovoliunnul  24576  volfiniun  24616  iundisj  24617  iunmbl2  24626  volsup2  24674  vitalilem2  24678  ismbf3d  24723  mbfaddlem  24729  mbfsup  24733  i1faddlem  24762  i1fmullem  24763  elaa  25381  numedglnl  27417  clwwlknun  28377  fusgreg2wsp  28601  iunin1f  30798  ssiun3  30799  iunpreima  30805  iundisjf  30829  unipreima  30882  aciunf1lem  30901  ofpreima  30904  iundisjfi  31019  fsumiunle  31045  gsumpart  31217  locfinreflem  31692  esum2dlem  31960  esum2d  31961  esumiun  31962  eulerpartlemgh  32245  dstfrvunirn  32341  reprsuc  32495  reprdifc  32507  bnj1405  32716  bnj916  32813  bnj983  32831  bnj1398  32914  bnj1417  32921  bnj1498  32941  fmlan0  33253  mclsppslem  33445  ttrclselem2  33712  oldlim  33996  colinearex  34289  neibastop2lem  34476  rdgellim  35474  exrecfnlem  35477  rabiun  35677  iundif1  35678  volsupnfl  35749  istotbnd3  35856  sstotbnd  35860  sstotbnd3  35861  prdstotbnd  35879  cntotbnd  35881  heiborlem3  35898  heibor  35906  pclfinN  37841  pclcmpatN  37842  lcfrvalsnN  39482  lcfrlem5  39487  lcfrlem6  39488  lcfrlem16  39499  lcfrlem27  39510  lcfrlem37  39520  lcfr  39526  mapdrvallem2  39586  cnviun  41147  imaiun1  41148  coiun1  41149  ss2iundf  41156  eliunov2  41176  iunconnlem2  42444  iunincfi  42533  eliuniin  42538  eliuniin2  42558  eliunid  42588  unirnmap  42637  unirnmapsn  42643  ssmapsn  42645  iunmapsn  42646  iuneqfzuzlem  42763  allbutfi  42823  fsumiunss  43006  fnlimfvre  43105  cnrefiisplem  43260  dvnprodlem1  43377  dvnprodlem2  43378  fourierdlem80  43617  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0iunmpt  43846  iundjiun  43888  meaiininclem  43914  hoicvr  43976  hoidmv1lelem3  44021  hoidmv1le  44022  hoidmvlelem3  44025  hspmbllem2  44055  opnvonmbllem2  44061  iunhoiioolem  44103  smfaddlem1  44185  smflimlem2  44194  smfmullem4  44215  smflimmpt  44230  smflimsuplem7  44246  smflimsuplem8  44247  smflimsupmpt  44249  smfliminfmpt  44252  fsetsniunop  44430  otiunsndisjX  44658  iccpartiun  44774  iunord  46268