Theorem eliun 4908

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 3426	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3426	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3201	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2825	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3216	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4906	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3589	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 383	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 209   = wceq 1543   ∈ wcel 2110  ∃wrex 3062  Vcvv 3408  ∪ ciun 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-v 3410  df-iun 4906

This theorem is referenced by:  eliuni  4910  iuncom  4911  iuncom4  4912  iunconst  4913  iuneqconst  4915  iuniin  4916  iinssiun  4917  iunss1  4918  ss2iun  4922  dfiun2g  4940  ssiun  4955  ssiun2  4956  iunab  4960  iun0  4970  0iun  4971  iunn0  4975  iunin2  4979  iundif2  4982  iindif2  4985  iunxsng  4998  iunxsngf  5000  iunun  5001  iunxun  5002  iunxdif3  5003  iunxiun  5005  iunpwss  5015  disjiun  5040  disjiund  5043  disjxiun  5050  triun  5174  otiunsndisj  5403  xpiundi  5619  xpiundir  5620  iunxpf  5717  cnvuni  5755  dmiun  5782  dmuni  5783  rniun  6011  xpdifid  6031  dfco2  6109  dfco2a  6110  coiun  6120  imaiun  7058  eluniima  7063  iunpw  7556  fiun  7716  f1iun  7717  opabex3d  7738  opabex3rd  7739  opabex3  7740  wfrdmcl  8063  onoviun  8080  smoiun  8098  oalimcl  8288  oaass  8289  oarec  8290  omordlim  8305  omlimcl  8306  omeulem1  8310  oelimcl  8328  oeeulem  8329  oaabs2  8374  omabs  8376  dffi3  9047  ixpiunwdom  9206  eltrpred  9331  dftrpred3g  9339  trpredrec  9342  trcl  9344  r1ordg  9394  r1pwss  9400  rankr1ai  9414  r1elss  9422  fseqenlem2  9639  infpwfien  9676  cardaleph  9703  ackbij2  9857  cfsmolem  9884  alephsing  9890  hsmexlem2  10041  ac6c4  10095  ttukeylem6  10128  iunfo  10153  iundom2g  10154  konigthlem  10182  alephreg  10196  pwcfsdom  10197  pwfseqlem3  10274  inar1  10389  inatsk  10392  fsuppmapnn0fiub  13564  wrdval  14072  s3iunsndisj  14531  dfrtrclrec2  14621  fsum2dlem  15334  fsumcom2  15338  fsumiun  15385  fprod2dlem  15542  fprodcom2  15546  prmreclem5  16473  imasaddfnlem  17033  imasvscafn  17042  smndex1basss  18332  smndex1mgm  18334  smndex1mndlem  18336  smndex1n0mnd  18339  efgsfo  19129  frgpnabllem1  19258  lssats2  20037  lbsextlem2  20196  lbsextlem3  20197  islpidl  20284  iunocv  20643  iunconnlem  22324  iunconn  22325  locfincmp  22423  alexsubALTlem3  22946  ptcmplem3  22951  imasdsf1olem  23271  zcld  23710  ovolfioo  24364  ovolficc  24365  ovoliunlem2  24400  ovoliunnul  24404  volfiniun  24444  iundisj  24445  iunmbl2  24454  volsup2  24502  vitalilem2  24506  ismbf3d  24551  mbfaddlem  24557  mbfsup  24561  i1faddlem  24590  i1fmullem  24591  elaa  25209  numedglnl  27235  clwwlknun  28195  fusgreg2wsp  28419  iunin1f  30616  ssiun3  30617  iunpreima  30623  iundisjf  30647  unipreima  30700  aciunf1lem  30719  ofpreima  30722  iundisjfi  30837  fsumiunle  30863  gsumpart  31034  locfinreflem  31504  esum2dlem  31772  esum2d  31773  esumiun  31774  eulerpartlemgh  32057  dstfrvunirn  32153  reprsuc  32307  reprdifc  32319  bnj1405  32529  bnj916  32626  bnj983  32644  bnj1398  32727  bnj1417  32734  bnj1498  32754  fmlan0  33066  mclsppslem  33258  oldlim  33806  colinearex  34099  neibastop2lem  34286  rdgellim  35284  exrecfnlem  35287  rabiun  35487  iundif1  35488  volsupnfl  35559  istotbnd3  35666  sstotbnd  35670  sstotbnd3  35671  prdstotbnd  35689  cntotbnd  35691  heiborlem3  35708  heibor  35716  pclfinN  37651  pclcmpatN  37652  lcfrvalsnN  39292  lcfrlem5  39297  lcfrlem6  39298  lcfrlem16  39309  lcfrlem27  39320  lcfrlem37  39330  lcfr  39336  mapdrvallem2  39396  cnviun  40935  imaiun1  40936  coiun1  40937  ss2iundf  40944  eliunov2  40964  iunconnlem2  42228  iunincfi  42317  eliuniin  42322  eliuniin2  42342  eliunid  42372  unirnmap  42421  unirnmapsn  42427  ssmapsn  42429  iunmapsn  42430  iuneqfzuzlem  42546  allbutfi  42606  fsumiunss  42791  fnlimfvre  42890  cnrefiisplem  43045  dvnprodlem1  43162  dvnprodlem2  43163  fourierdlem80  43402  sge0iunmptlemfi  43626  sge0iunmptlemre  43628  sge0iunmpt  43631  iundjiun  43673  meaiininclem  43699  hoicvr  43761  hoidmv1lelem3  43806  hoidmv1le  43807  hoidmvlelem3  43810  hspmbllem2  43840  opnvonmbllem2  43846  iunhoiioolem  43888  smfaddlem1  43970  smflimlem2  43979  smfmullem4  44000  smflimmpt  44015  smflimsuplem7  44031  smflimsuplem8  44032  smflimsupmpt  44034  smfliminfmpt  44037  fsetsniunop  44215  otiunsndisjX  44443  iccpartiun  44559  iunord  46053