Theorem eliun 4994

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 3491	. 2 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 → 𝐴 ∈ V)
2		elex 3491	. . 3 ⊢ (𝐴 ∈ 𝐶 → 𝐴 ∈ V)
3	2	rexlimivw 3150	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶 → 𝐴 ∈ V)
4		eleq1 2820	. . . 4 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶))
5	4	rexbidv 3177	. . 3 ⊢ (𝑦 = 𝐴 → (∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
6		df-iun 4992	. . 3 ⊢ ∪ 𝑥 ∈ 𝐵 𝐶 = {𝑦 ∣ ∃𝑥 ∈ 𝐵 𝑦 ∈ 𝐶}
7	5, 6	elab2g 3666	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶))
8	1, 3, 7	pm5.21nii 379	1 ⊢ (𝐴 ∈ ∪ 𝑥 ∈ 𝐵 𝐶 ↔ ∃𝑥 ∈ 𝐵 𝐴 ∈ 𝐶)

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  ∃wrex 3069  Vcvv 3473  ∪ ciun 4990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3475  df-iun 4992

This theorem is referenced by:  eliuni  4996  iuncom  4997  iuncom4  4998  iunconst  4999  iuneqconst  5001  iuniin  5002  iinssiun  5003  iunss1  5004  ss2iun  5008  dfiun2gOLD  5027  ssiun  5042  ssiun2  5043  iunab  5047  iun0  5058  0iun  5059  iunn0  5063  iunin2  5067  iundif2  5070  iindif2  5073  iunxsng  5086  iunxsngf  5088  iunun  5089  iunxun  5090  iunxdif3  5091  iunxiun  5093  iunpwss  5103  disjiun  5128  disjiund  5131  disjxiun  5138  triun  5273  otiunsndisj  5513  xpiundi  5738  xpiundir  5739  iunxpf  5840  cnvuni  5878  dmiun  5905  dmuni  5906  rniun  6136  xpdifid  6156  dfco2  6233  dfco2a  6234  coiun  6244  imaiun  7228  eluniima  7233  iunpw  7741  fiun  7911  f1iun  7912  opabex3d  7934  opabex3rd  7935  opabex3  7936  wfrdmclOLD  8299  onoviun  8325  smoiun  8343  oalimcl  8543  oaass  8544  oarec  8545  omordlim  8560  omlimcl  8561  omeulem1  8565  oelimcl  8583  oeeulem  8584  oaabs2  8631  omabs  8633  dffi3  9408  ixpiunwdom  9567  ttrclselem2  9703  trcl  9705  r1ordg  9755  r1pwss  9761  rankr1ai  9775  r1elss  9783  fseqenlem2  10002  infpwfien  10039  cardaleph  10066  ackbij2  10220  cfsmolem  10247  alephsing  10253  hsmexlem2  10404  ac6c4  10458  ttukeylem6  10491  iunfo  10516  iundom2g  10517  konigthlem  10545  alephreg  10559  pwcfsdom  10560  pwfseqlem3  10637  inar1  10752  inatsk  10755  fsuppmapnn0fiub  13938  wrdval  14449  s3iunsndisj  14897  dfrtrclrec2  14987  fsum2dlem  15698  fsumcom2  15702  fsumiun  15749  fprod2dlem  15906  fprodcom2  15910  prmreclem5  16835  imasaddfnlem  17456  imasvscafn  17465  smndex1basss  18761  smndex1mgm  18763  smndex1mndlem  18765  smndex1n0mnd  18768  efgsfo  19571  frgpnabllem1  19701  lssats2  20560  lbsextlem2  20721  lbsextlem3  20722  islpidl  20820  iunocv  21167  iunconnlem  22860  iunconn  22861  locfincmp  22959  alexsubALTlem3  23482  ptcmplem3  23487  imasdsf1olem  23808  zcld  24258  ovolfioo  24913  ovolficc  24914  ovoliunlem2  24949  ovoliunnul  24953  volfiniun  24993  iundisj  24994  iunmbl2  25003  volsup2  25051  vitalilem2  25055  ismbf3d  25100  mbfaddlem  25106  mbfsup  25110  i1faddlem  25139  i1fmullem  25140  elaa  25758  oldlim  27304  numedglnl  28269  clwwlknun  29230  fusgreg2wsp  29454  iunin1f  31654  ssiun3  31655  iunpreima  31661  iundisjf  31685  unipreima  31738  aciunf1lem  31756  ofpreima  31759  iundisjfi  31878  fsumiunle  31906  gsumpart  32078  elirng  32588  irngnzply1  32593  locfinreflem  32651  esum2dlem  32921  esum2d  32922  esumiun  32923  eulerpartlemgh  33208  dstfrvunirn  33304  reprsuc  33458  reprdifc  33470  bnj1405  33678  bnj916  33775  bnj983  33793  bnj1398  33876  bnj1417  33883  bnj1498  33903  fmlan0  34213  mclsppslem  34405  colinearex  34862  neibastop2lem  35049  rdgellim  36061  exrecfnlem  36064  rabiun  36265  iundif1  36266  volsupnfl  36337  istotbnd3  36444  sstotbnd  36448  sstotbnd3  36449  prdstotbnd  36467  cntotbnd  36469  heiborlem3  36486  heibor  36494  pclfinN  38576  pclcmpatN  38577  lcfrvalsnN  40217  lcfrlem5  40222  lcfrlem6  40223  lcfrlem16  40234  lcfrlem27  40245  lcfrlem37  40255  lcfr  40261  mapdrvallem2  40321  cnviun  42172  imaiun1  42173  coiun1  42174  ss2iundf  42181  eliunov2  42201  iunconnlem2  43467  iunincfi  43554  eliuniin  43559  eliuniin2  43580  eliunid  43610  iindif2f  43625  eliund  43628  unirnmap  43678  unirnmapsn  43684  ssmapsn  43686  iunmapsn  43687  iuneqfzuzlem  43817  allbutfi  43876  fsumiunss  44064  fnlimfvre  44163  cnrefiisplem  44318  dvnprodlem1  44435  dvnprodlem2  44436  fourierdlem80  44675  sge0iunmptlemfi  44902  sge0iunmptlemre  44904  sge0iunmpt  44907  iundjiun  44949  meaiininclem  44975  hoicvr  45037  hoidmv1lelem3  45082  hoidmv1le  45083  hoidmvlelem3  45086  hspmbllem2  45116  opnvonmbllem2  45122  iunhoiioolem  45164  smfaddlem1  45252  smflimlem2  45261  smfmullem4  45283  smflimmpt  45299  smflimsuplem7  45315  smflimsuplem8  45316  smflimsupmpt  45318  smfliminfmpt  45321  fsupdm  45331  finfdm  45335  fsetsniunop  45531  otiunsndisjX  45759  iccpartiun  45874  iunord  47369