Theorem eliun 4999

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 3498	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3498	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3148	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2826	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3176	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4997	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3682	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 378	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105  ∃wrex 3067  Vcvv 3477  ∪ ciun 4995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rex 3068  df-v 3479  df-iun 4997

This theorem is referenced by:  eliuni  5001  eliund  5002  iuncom  5003  iuncom4  5004  iunconst  5005  iuneqconst  5007  iuniin  5008  iinssiun  5009  iunss1  5010  ss2iun  5014  nfiu1  5031  dfiun2gOLD  5035  ssiun  5050  ssiun2  5051  iunab  5055  iun0  5066  0iun  5067  iunn0  5071  iunin2  5075  iundif2  5078  iindif2  5081  iunxsng  5094  iunxsngf  5096  iunun  5097  iunxun  5098  iunxdif3  5099  iunxiun  5101  iunpwss  5111  disjiun  5135  disjiund  5138  disjxiun  5144  triun  5279  otiunsndisj  5529  xpiundi  5758  xpiundir  5759  iunxpf  5861  cnvuni  5899  dmiun  5926  dmuni  5927  rniun  6169  xpdifid  6189  dfco2  6266  dfco2a  6267  coiun  6277  imaiun  7264  eluniima  7269  iunpw  7789  fiun  7965  f1iun  7966  opabex3d  7988  opabex3rd  7989  opabex3  7990  wfrdmclOLD  8355  onoviun  8381  smoiun  8399  oalimcl  8596  oaass  8597  oarec  8598  omordlim  8613  omlimcl  8614  omeulem1  8618  oelimcl  8636  oeeulem  8637  oaabs2  8685  omabs  8687  dffi3  9468  ixpiunwdom  9627  ttrclselem2  9763  trcl  9765  r1ordg  9815  r1pwss  9821  rankr1ai  9835  r1elss  9843  fseqenlem2  10062  infpwfien  10099  cardaleph  10126  ackbij2  10279  cfsmolem  10307  alephsing  10313  hsmexlem2  10464  ac6c4  10518  ttukeylem6  10551  iunfo  10576  iundom2g  10577  konigthlem  10605  alephreg  10619  pwcfsdom  10620  pwfseqlem3  10697  inar1  10812  inatsk  10815  fsuppmapnn0fiub  14028  wrdval  14551  s3iunsndisj  15003  dfrtrclrec2  15093  fsum2dlem  15802  fsumcom2  15806  fsumiun  15853  fprod2dlem  16012  fprodcom2  16016  prmreclem5  16953  imasaddfnlem  17574  imasvscafn  17583  smndex1basss  18930  smndex1mgm  18932  smndex1mndlem  18934  smndex1n0mnd  18937  efgsfo  19771  frgpnabllem1  19905  lssats2  21015  lbsextlem2  21178  lbsextlem3  21179  islpidl  21352  pzriprnglem10  21518  pzriprnglem12  21520  pzriprnglem13  21521  pzriprnglem14  21522  iunocv  21716  iunconnlem  23450  iunconn  23451  locfincmp  23549  alexsubALTlem3  24072  ptcmplem3  24077  imasdsf1olem  24398  zcld  24848  ovolfioo  25515  ovolficc  25516  ovoliunlem2  25551  ovoliunnul  25555  volfiniun  25595  iundisj  25596  iunmbl2  25605  volsup2  25653  vitalilem2  25657  ismbf3d  25702  mbfaddlem  25708  mbfsup  25712  i1faddlem  25741  i1fmullem  25742  elaa  26372  oldlim  27939  precsexlem10  28254  precsexlem11  28255  numedglnl  29175  clwwlknun  30140  fusgreg2wsp  30364  iunin1f  32577  ssiun3  32578  iunpreima  32584  iundisjf  32608  unipreima  32659  aciunf1lem  32678  ofpreima  32681  iundisjfi  32803  fsumiunle  32835  gsumpart  33042  gsumwrd2dccatlem  33051  elirng  33700  irngnzply1  33705  irngnminplynz  33719  constrconj  33749  locfinreflem  33800  esum2dlem  34072  esum2d  34073  esumiun  34074  eulerpartlemgh  34359  dstfrvunirn  34455  reprsuc  34608  reprdifc  34620  bnj1405  34828  bnj916  34925  bnj983  34943  bnj1398  35026  bnj1417  35033  bnj1498  35053  fmlan0  35375  mclsppslem  35567  colinearex  36041  neibastop2lem  36342  weiunlem2  36445  rdgellim  37358  exrecfnlem  37361  rabiun  37579  iundif1  37580  volsupnfl  37651  istotbnd3  37757  sstotbnd  37761  sstotbnd3  37762  prdstotbnd  37780  cntotbnd  37782  heiborlem3  37799  heibor  37807  pclfinN  39882  pclcmpatN  39883  lcfrvalsnN  41523  lcfrlem5  41528  lcfrlem6  41529  lcfrlem16  41540  lcfrlem27  41551  lcfrlem37  41561  lcfr  41567  mapdrvallem2  41627  grpods  42175  cnviun  43639  imaiun1  43640  coiun1  43641  ss2iundf  43648  eliunov2  43668  iunconnlem2  44932  iunincfi  45033  eliuniin  45038  eliuniin2  45059  eliunid  45089  iindif2f  45102  unirnmap  45150  unirnmapsn  45156  ssmapsn  45158  iunmapsn  45159  iuneqfzuzlem  45283  allbutfi  45342  fsumiunss  45530  fnlimfvre  45629  cnrefiisplem  45784  dvnprodlem1  45901  dvnprodlem2  45902  fourierdlem80  46141  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0iunmpt  46373  iundjiun  46415  meaiininclem  46441  hoicvr  46503  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem3  46552  hspmbllem2  46582  opnvonmbllem2  46588  iunhoiioolem  46630  smfaddlem1  46718  smflimlem2  46727  smfmullem4  46749  smflimmpt  46765  smflimsuplem7  46781  smflimsuplem8  46782  smflimsupmpt  46784  smfliminfmpt  46787  fsupdm  46797  finfdm  46801  fsetsniunop  46998  otiunsndisjX  47228  iccpartiun  47358  stgredgiun  47860  iunord  48906