Theorem eliun 4943

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 3465	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3465	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3149	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2840	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3176	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4941	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3630	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 380	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 208   = wceq 1550   ∈ wcel 2132  ∃wrex 3076  Vcvv 3444  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rex 3077  df-v 3446  df-iun 4941

This theorem is referenced by:  eliuni  4945  eliund  4946  iuncom  4947  iuncom4  4948  iunconst  4949  iuneqconst  4951  iuniin  4952  iinssiun  4953  iunss1  4954  ss2iun  4958  nfiu1  4975  iunssf  4990  iunss  4992  ssiun  4994  ssiun2  4995  iunab  4999  iun0  5009  0iun  5010  iunn0  5014  iunin2  5018  iundif2  5021  iindif2  5024  iunxsng  5037  iunxsngf  5039  iunun  5040  iunxun  5041  iunxdif3  5042  iunxiun  5044  iunpwss  5054  disjiun  5078  disjiund  5081  disjxiun  5087  triun  5212  otiunsndisj  5479  xpiundi  5707  xpiundir  5708  iunxpf  5809  cnvuni  5851  dmiun  5878  dmuni  5879  rniun  6118  xpdifid  6139  dfco2  6217  dfco2a  6218  coiun  6229  imaiun  7214  eluniima  7219  iunpw  7739  fiun  7909  f1iun  7910  opabex3d  7931  opabex3rd  7932  opabex3  7933  onoviun  8298  smoiun  8316  oalimcl  8513  oaass  8514  oarec  8515  omordlim  8530  omlimcl  8531  omeulem1  8535  oelimcl  8554  oeeulem  8555  oaabs2  8603  omabs  8605  dffi3  9363  ixpiunwdom  9524  ttrclselem2  9667  trcl  9669  r1ordg  9722  r1pwss  9728  rankr1ai  9742  r1elss  9750  fseqenlem2  9967  infpwfien  10004  cardaleph  10031  ackbij2  10184  cfsmolem  10213  alephsing  10219  hsmexlem2  10370  ac6c4  10424  ttukeylem6  10457  iunfo  10482  iundom2g  10483  konigthlem  10512  alephreg  10526  pwcfsdom  10527  pwfseqlem3  10604  inar1  10719  inatsk  10722  fsuppmapnn0fiub  13990  wrdval  14515  s3iunsndisj  14967  dfrtrclrec2  15057  fsum2dlem  15769  fsumcom2  15773  fsumiun  15821  fprod2dlem  15982  fprodcom2  15986  prmreclem5  16928  imasaddfnlem  17530  imasvscafn  17539  smndex1basss  18914  smndex1mgm  18916  smndex1mndlem  18918  smndex1n0mnd  18921  efgsfo  19751  frgpnabllem1  19885  lssats2  21036  lbsextlem2  21198  lbsextlem3  21199  islpidl  21364  pzriprnglem10  21511  pzriprnglem12  21513  pzriprnglem13  21514  pzriprnglem14  21515  iunocv  21702  iunconnlem  23456  iunconn  23457  locfincmp  23555  alexsubALTlem3  24078  ptcmplem3  24083  imasdsf1olem  24402  zcld  24843  ovolfioo  25498  ovolficc  25499  ovoliunlem2  25534  ovoliunnul  25538  volfiniun  25578  iundisj  25579  iunmbl2  25588  volsup2  25636  vitalilem2  25640  ismbf3d  25685  mbfaddlem  25691  mbfsup  25695  i1faddlem  25724  i1fmullem  25725  elaa  26346  oldlim  27946  precsexlem10  28275  precsexlem11  28276  numedglnl  29280  clwwlknun  30249  fusgreg2wsp  30473  iunin1f  32695  ssiun3  32696  iunpreima  32702  iundisjf  32727  unipreima  32784  aciunf1lem  32803  ofpreima  32806  iundisjfi  32937  fsumiunle  32970  gsumpart  33193  gsumwrd2dccatlem  33207  elirng  33927  irngnzply1  33932  irngnminplynz  33953  constrconj  33986  locfinreflem  34081  esum2dlem  34333  esum2d  34334  esumiun  34335  eulerpartlemgh  34619  dstfrvunirn  34716  reprsuc  34856  reprdifc  34868  bnj1405  35078  bnj916  35175  bnj983  35193  bnj1398  35276  bnj1417  35283  bnj1498  35303  fmlan0  35679  mclsppslem  35871  colinearex  36348  neibastop2lem  36658  weiunlem  36761  ttctr  36791  rdgellim  37808  exrecfnlem  37811  rabiun  38030  iundif1  38031  volsupnfl  38102  istotbnd3  38208  sstotbnd  38212  sstotbnd3  38213  prdstotbnd  38231  cntotbnd  38233  heiborlem3  38250  heibor  38258  pclfinN  40462  pclcmpatN  40463  lcfrvalsnN  42103  lcfrlem5  42108  lcfrlem6  42109  lcfrlem16  42120  lcfrlem27  42131  lcfrlem37  42141  lcfr  42147  mapdrvallem2  42207  grpods  42749  cnviun  44164  imaiun1  44165  coiun1  44166  ss2iundf  44173  eliunov2  44193  iunconnlem2  45448  iunincfi  45610  eliuniin  45615  eliuniin2  45636  eliunid  45663  iindif2f  45676  unirnmap  45722  unirnmapsn  45728  ssmapsn  45730  iunmapsn  45731  iuneqfzuzlem  45848  allbutfi  45906  fsumiunss  46089  fnlimfvre  46186  cnrefiisplem  46341  dvnprodlem1  46458  dvnprodlem2  46459  fourierdlem80  46698  sge0iunmptlemfi  46925  sge0iunmptlemre  46927  sge0iunmpt  46930  iundjiun  46972  meaiininclem  46998  hoidmv1lelem3  47105  hoidmv1le  47106  hoidmvlelem3  47109  hspmbllem2  47139  opnvonmbllem2  47145  iunhoiioolem  47187  smfaddlem1  47275  smflimlem2  47284  smfmullem4  47306  smflimmpt  47322  smflimsuplem7  47338  smflimsuplem8  47339  smflimsupmpt  47341  smfliminfmpt  47344  fsupdm  47354  finfdm  47358  fsetsniunop  47581  otiunsndisjX  47811  iccpartiun  47978  stgredgiun  48518  iunord  50235