Theorem eliun 4948

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 3459	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3126	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2816	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3153	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4946	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3638	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  ∃wrex 3053  Vcvv 3438  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3440  df-iun 4946

This theorem is referenced by:  eliuni  4950  eliund  4951  iuncom  4952  iuncom4  4953  iunconst  4954  iuneqconst  4956  iuniin  4957  iinssiun  4958  iunss1  4959  ss2iun  4963  nfiu1  4980  ssiun  4998  ssiun2  4999  iunab  5003  iun0  5014  0iun  5015  iunn0  5019  iunin2  5023  iundif2  5026  iindif2  5029  iunxsng  5042  iunxsngf  5044  iunun  5045  iunxun  5046  iunxdif3  5047  iunxiun  5049  iunpwss  5059  disjiun  5083  disjiund  5086  disjxiun  5092  triun  5216  otiunsndisj  5467  xpiundi  5694  xpiundir  5695  iunxpf  5795  cnvuni  5833  dmiun  5860  dmuni  5861  rniun  6100  xpdifid  6121  dfco2  6198  dfco2a  6199  coiun  6209  imaiun  7185  eluniima  7190  iunpw  7711  fiun  7885  f1iun  7886  opabex3d  7907  opabex3rd  7908  opabex3  7909  onoviun  8273  smoiun  8291  oalimcl  8485  oaass  8486  oarec  8487  omordlim  8502  omlimcl  8503  omeulem1  8507  oelimcl  8525  oeeulem  8526  oaabs2  8574  omabs  8576  dffi3  9340  ixpiunwdom  9501  ttrclselem2  9641  trcl  9643  r1ordg  9693  r1pwss  9699  rankr1ai  9713  r1elss  9721  fseqenlem2  9938  infpwfien  9975  cardaleph  10002  ackbij2  10155  cfsmolem  10183  alephsing  10189  hsmexlem2  10340  ac6c4  10394  ttukeylem6  10427  iunfo  10452  iundom2g  10453  konigthlem  10481  alephreg  10495  pwcfsdom  10496  pwfseqlem3  10573  inar1  10688  inatsk  10691  fsuppmapnn0fiub  13916  wrdval  14441  s3iunsndisj  14893  dfrtrclrec2  14983  fsum2dlem  15695  fsumcom2  15699  fsumiun  15746  fprod2dlem  15905  fprodcom2  15909  prmreclem5  16850  imasaddfnlem  17450  imasvscafn  17459  smndex1basss  18797  smndex1mgm  18799  smndex1mndlem  18801  smndex1n0mnd  18804  efgsfo  19636  frgpnabllem1  19770  lssats2  20921  lbsextlem2  21084  lbsextlem3  21085  islpidl  21250  pzriprnglem10  21415  pzriprnglem12  21417  pzriprnglem13  21418  pzriprnglem14  21419  iunocv  21606  iunconnlem  23330  iunconn  23331  locfincmp  23429  alexsubALTlem3  23952  ptcmplem3  23957  imasdsf1olem  24277  zcld  24718  ovolfioo  25384  ovolficc  25385  ovoliunlem2  25420  ovoliunnul  25424  volfiniun  25464  iundisj  25465  iunmbl2  25474  volsup2  25522  vitalilem2  25526  ismbf3d  25571  mbfaddlem  25577  mbfsup  25581  i1faddlem  25610  i1fmullem  25611  elaa  26240  oldlim  27819  precsexlem10  28141  precsexlem11  28142  numedglnl  29107  clwwlknun  30074  fusgreg2wsp  30298  iunin1f  32519  ssiun3  32520  iunpreima  32526  iundisjf  32551  unipreima  32600  aciunf1lem  32619  ofpreima  32622  iundisjfi  32752  fsumiunle  32787  gsumpart  33023  gsumwrd2dccatlem  33032  elirng  33657  irngnzply1  33662  irngnminplynz  33678  constrconj  33711  locfinreflem  33806  esum2dlem  34058  esum2d  34059  esumiun  34060  eulerpartlemgh  34345  dstfrvunirn  34442  reprsuc  34582  reprdifc  34594  bnj1405  34802  bnj916  34899  bnj983  34917  bnj1398  35000  bnj1417  35007  bnj1498  35027  fmlan0  35363  mclsppslem  35555  colinearex  36033  neibastop2lem  36333  weiunlem2  36436  rdgellim  37349  exrecfnlem  37352  rabiun  37572  iundif1  37573  volsupnfl  37644  istotbnd3  37750  sstotbnd  37754  sstotbnd3  37755  prdstotbnd  37773  cntotbnd  37775  heiborlem3  37792  heibor  37800  pclfinN  39879  pclcmpatN  39880  lcfrvalsnN  41520  lcfrlem5  41525  lcfrlem6  41526  lcfrlem16  41537  lcfrlem27  41548  lcfrlem37  41558  lcfr  41564  mapdrvallem2  41624  grpods  42167  cnviun  43623  imaiun1  43624  coiun1  43625  ss2iundf  43632  eliunov2  43652  iunconnlem2  44908  iunincfi  45072  eliuniin  45077  eliuniin2  45098  eliunid  45125  iindif2f  45138  unirnmap  45186  unirnmapsn  45192  ssmapsn  45194  iunmapsn  45195  iuneqfzuzlem  45314  allbutfi  45373  fsumiunss  45557  fnlimfvre  45656  cnrefiisplem  45811  dvnprodlem1  45928  dvnprodlem2  45929  fourierdlem80  46168  sge0iunmptlemfi  46395  sge0iunmptlemre  46397  sge0iunmpt  46400  iundjiun  46442  meaiininclem  46468  hoicvr  46530  hoidmv1lelem3  46575  hoidmv1le  46576  hoidmvlelem3  46579  hspmbllem2  46609  opnvonmbllem2  46615  iunhoiioolem  46657  smfaddlem1  46745  smflimlem2  46754  smfmullem4  46776  smflimmpt  46792  smflimsuplem7  46808  smflimsuplem8  46809  smflimsupmpt  46811  smfliminfmpt  46814  fsupdm  46824  finfdm  46828  fsetsniunop  47034  otiunsndisjX  47264  iccpartiun  47419  stgredgiun  47941  iunord  49649