Theorem eliun 4954

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 3471	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3471	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3159	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2848	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3186	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4952	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3633	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 381	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-iun 4952

This theorem is used by:  eliuni  4956  eliund  4957  iuncom  4958  iuncom4  4959  iunconst  4960  iuneqconst  4962  iuniin  4963  iinssiun  4964  iunss1  4965  ss2iun  4969  nfiu1  4985  iunssf  5000  iunss  5002  ssiun  5004  ssiun2  5005  iunab  5009  iun0  5019  0iun  5020  iunn0  5024  iunin2  5028  iundif2  5031  iindif2  5036  iunxsng  5049  iunxsngf  5051  iunun  5052  iunxun  5053  iunxdif3  5054  iunxiun  5056  iunpwss  5066  disjiun  5090  disjiund  5093  disjxiun  5099  triun  5226  otiunsndisj  5489  xpiundi  5718  xpiundir  5719  iunxpf  5822  cnvuni  5864  dmiun  5891  dmuni  5892  rniun  6133  xpdifid  6154  xpdifcnvepel  6155  dfco2  6235  dfco2a  6236  coiun  6247  iunpreima  7056  imaiun  7237  eluniima  7242  iunpw  7768  fiun  7938  f1iun  7939  opabex3d  7960  opabex3rd  7961  opabex3  7962  onoviun  8329  smoiun  8347  oalimcl  8546  oaass  8547  oarec  8548  omordlim  8563  omlimcl  8564  omeulem1  8568  oelimcl  8587  oeeulem  8588  oaabs2  8636  omabs  8638  dffi3  9401  ixpiunwdom  9562  ttrclselem2  9705  trcl  9707  r1ordg  9760  r1pwss  9766  rankr1ai  9780  r1elss  9788  fseqenlem2  10075  infpwfien  10112  cardaleph  10139  ackbij2  10291  cfsmolem  10319  alephsing  10325  hsmexlem2  10476  ac6c4  10530  ttukeylem6  10563  iunfo  10594  iundom2g  10595  konigthlem  10624  alephreg  10638  pwcfsdom  10639  pwfseqlem3  10716  inar1  10831  inatsk  10834  fsuppmapnn0fiub  14102  wrdval  14628  s3iunsndisj  15088  dfrtrclrec2  15178  fsum2dlem  15903  fsumcom2  15907  fsumiun  15955  fprod2dlem  16114  fprodcom2  16118  prmreclem5  17059  imasaddfnlem  17661  imasvscafn  17670  smndex1basss  19065  smndex1mgm  19067  smndex1mndlem  19069  smndex1n0mnd  19072  efgsfo  19914  frgpnabllem1  20048  lssats2  21236  lbsextlem2  21398  lbsextlem3  21399  islpidl  21610  pzriprnglem10  21757  pzriprnglem12  21759  pzriprnglem13  21760  pzriprnglem14  21761  iunocv  21948  iunconnlem  23706  iunconn  23707  locfincmp  23806  alexsubALTlem3  24329  ptcmplem3  24334  imasdsf1olem  24653  zcld  25094  ovolfioo  25749  ovolficc  25750  ovoliunlem2  25785  ovoliunnul  25789  volfiniun  25829  iundisj  25830  iunmbl2  25839  volsup2  25887  vitalilem2  25891  ismbf3d  25936  mbfaddlem  25942  mbfsup  25946  i1faddlem  25975  i1fmullem  25976  elaa  26602  oldlim  28206  precsexlem10  28535  precsexlem11  28536  numedglnl  29655  clwwlknun  30636  fusgreg2wsp  30870  iunin1f  33085  ssiun3  33086  iundisjf  33116  unipreima  33170  aciunf1lem  33189  ofpreima  33192  iundisjfi  33321  fsumiunle  33353  gsumpart  33557  gsumwrd2dccatlem  33571  elirng  34251  irngnzply1  34256  irngnminplynz  34277  constrconj  34310  locfinreflem  34405  esum2dlem  34657  esum2d  34658  esumiun  34659  eulerpartlemgh  34944  dstfrvunirn  35041  reprsuc  35178  reprdifc  35190  bnj1405  35400  bnj916  35497  bnj983  35515  bnj1398  35598  bnj1417  35605  bnj1498  35625  fmlan0  36077  mclsppslem  36269  colinearex  36747  neibastop2lem  37070  weiunlem  37173  ttctr  37203  rdgellim  38219  exrecfnlem  38222  rabiun  38441  iundif1  38442  volsupnfl  38503  istotbnd3  38625  sstotbnd  38629  sstotbnd3  38630  prdstotbnd  38648  cntotbnd  38650  heiborlem3  38667  heibor  38675  pclfinN  40877  pclcmpatN  40878  lcfrvalsnN  42518  lcfrlem5  42523  lcfrlem6  42524  lcfrlem16  42535  lcfrlem27  42546  lcfrlem37  42556  lcfr  42562  mapdrvallem2  42622  grpods  43164  cnviun  44594  imaiun1  44595  coiun1  44596  ss2iundf  44603  eliunov2  44623  iunconnlem2  45861  iunincfi  46030  eliuniin  46035  eliuniin2  46056  eliunid  46083  iindif2f  46096  unirnmap  46142  unirnmapsn  46148  ssmapsn  46150  iunmapsn  46151  iuneqfzuzlem  46268  allbutfi  46326  fsumiunss  46509  fnlimfvre  46606  cnrefiisplem  46761  dvnprodlem1  46878  dvnprodlem2  46879  fourierdlem80  47118  sge0iunmptlemfi  47345  sge0iunmptlemre  47347  sge0iunmpt  47350  iundjiun  47392  meaiininclem  47418  hoidmv1lelem3  47525  hoidmv1le  47526  hoidmvlelem3  47529  hspmbllem2  47559  opnvonmbllem2  47565  iunhoiioolem  47607  smfaddlem1  47695  smflimlem2  47704  smfmullem4  47726  smflimmpt  47742  smflimsuplem7  47758  smflimsuplem8  47759  smflimsupmpt  47761  smfliminfmpt  47764  fsupdm  47774  finfdm  47778  fsetsniunop  48041  otiunsndisjX  48271  iccpartiun  48438  stgredgiun  48978  iunord  50706