Theorem eliun 4792

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 3427	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3427	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3221	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2847	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3236	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4790	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3578	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 371	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 198   = wceq 1507   ∈ wcel 2050  ∃wrex 3083  Vcvv 3409  ∪ ciun 4788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-v 3411  df-iun 4790

This theorem is referenced by:  eliuni  4794  iuncom  4795  iuncom4  4796  iunconst  4797  iuniin  4799  iinssiun  4800  iunss1  4801  ss2iun  4805  dfiun2g  4821  dfiun2gOLD  4822  ssiun  4832  ssiun2  4833  iunab  4837  iun0  4847  0iun  4848  iunn0  4851  iunin2  4855  iundif2  4858  iindif2  4861  iunxsng  4874  iunxsngf  4876  iunun  4877  iunxun  4878  iunxdif3  4879  iunxiun  4881  iunpwss  4891  disjiun  4913  disjiund  4916  disjxiun  4922  triun  5039  otiunsndisj  5262  xpiundi  5468  xpiundir  5469  iunxpf  5565  cnvuni  5603  dmiun  5628  dmuni  5629  rniun  5843  xpdifid  5862  dfco2  5934  dfco2a  5935  coiun  5945  imaiun  6827  eluniima  6832  iunpw  7307  fun11iun  7456  opabex3d  7476  opabex3rd  7477  opabex3  7478  wfrdmcl  7765  onoviun  7782  smoiun  7800  oalimcl  7985  oaass  7986  oarec  7987  omordlim  8002  omlimcl  8003  omeulem1  8007  oelimcl  8025  oeeulem  8026  oaabs2  8070  omabs  8072  dffi3  8688  ixpiunwdom  8848  trcl  8962  r1ordg  8999  r1pwss  9005  rankr1ai  9019  r1elss  9027  fseqenlem2  9243  infpwfien  9280  cardaleph  9307  ackbij2  9461  cfsmolem  9488  alephsing  9494  hsmexlem2  9645  ac6c4  9699  ttukeylem6  9732  iunfo  9757  iundom2g  9758  konigthlem  9786  alephreg  9800  pwcfsdom  9801  pwfseqlem3  9878  inar1  9993  inatsk  9996  fsuppmapnn0fiub  13172  wrdval  13673  s3iunsndisj  14187  dfrtrclrec2  14275  fsum2dlem  14983  fsumcom2  14987  fsumiun  15034  fprod2dlem  15192  fprodcom2  15196  prmreclem5  16110  imasaddfnlem  16655  imasvscafn  16664  efgsfo  18636  frgpnabllem1  18761  lssats2  19506  lbsextlem2  19665  lbsextlem3  19666  islpidl  19752  iunocv  20539  iunconnlem  21751  iunconn  21752  locfincmp  21850  alexsubALTlem3  22373  ptcmplem3  22378  imasdsf1olem  22698  zcld  23136  ovolfioo  23783  ovolficc  23784  ovoliunlem2  23819  ovoliunnul  23823  volfiniun  23863  iundisj  23864  iunmbl2  23873  volsup2  23921  vitalilem2  23925  ismbf3d  23970  mbfaddlem  23976  mbfsup  23980  i1faddlem  24009  i1fmullem  24010  elaa  24620  numedglnl  26644  clwwlknun  27652  fusgreg2wsp  27882  iunin1f  30092  ssiun3  30093  iunpreima  30099  iundisjf  30119  unipreima  30167  aciunf1lem  30183  ofpreima  30186  iundisjfi  30289  fsumiunle  30312  locfinreflem  30777  esum2dlem  31024  esum2d  31025  esumiun  31026  eulerpartlemgh  31310  dstfrvunirn  31407  reprsuc  31563  reprdifc  31575  bnj1405  31785  bnj916  31881  bnj983  31899  bnj1398  31980  bnj1417  31987  bnj1498  32007  mclsppslem  32379  eltrpred  32615  dftrpred3g  32622  trpredrec  32627  colinearex  33071  neibastop2lem  33258  rdgellim  34128  exrecfnlem  34131  rabiun  34335  iundif1  34336  volsupnfl  34407  istotbnd3  34520  sstotbnd  34524  sstotbnd3  34525  prdstotbnd  34543  cntotbnd  34545  heiborlem3  34562  heibor  34570  pclfinN  36510  pclcmpatN  36511  lcfrvalsnN  38151  lcfrlem5  38156  lcfrlem6  38157  lcfrlem16  38168  lcfrlem27  38179  lcfrlem37  38189  lcfr  38195  mapdrvallem2  38255  cnviun  39387  imaiun1  39388  coiun1  39389  ss2iundf  39396  eliunov2  39416  iunconnlem2  40717  iunincfi  40808  eliuniin  40814  eliuniin2  40836  eliunid  40868  unirnmap  40922  unirnmapsn  40928  ssmapsn  40930  iunmapsn  40931  iuneqfzuzlem  41056  allbutfi  41120  fsumiunss  41312  fnlimfvre  41411  cnrefiisplem  41566  dvnprodlem1  41686  dvnprodlem2  41687  fourierdlem80  41927  sge0iunmptlemfi  42151  sge0iunmptlemre  42153  sge0iunmpt  42156  iundjiun  42198  meaiininclem  42224  hoicvr  42286  hoidmv1lelem3  42331  hoidmv1le  42332  hoidmvlelem3  42335  hspmbllem2  42365  opnvonmbllem2  42371  iunhoiioolem  42413  smfaddlem1  42495  smflimlem2  42504  smfmullem4  42525  smflimmpt  42540  smflimsuplem7  42556  smflimsuplem8  42557  smflimsupmpt  42559  smfliminfmpt  42562  otiunsndisjX  42909  iccpartiun  42991  iunord  44171