Theorem eliun 4524

Description: Membership in indexed union. (Contributed by NM, 3-Sep-2003.)

Assertion

Ref	Expression
eliun	|- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Distinct variable group:   x, A

Allowed substitution hints:   B( x)   C( x)

Proof of Theorem eliun

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3212	. 2 |- ( A e. U_ x e. B C -> A e. _V )
2		elex 3212	. . 3 |- ( A e. C -> A e. _V )
3	2	rexlimivw 3029	. 2 |- ( E. x e. B A e. C -> A e. _V )
4		eleq1 2689	. . . 4 |- ( y = A -> ( y e. C <-> A e. C ) )
5	4	rexbidv 3052	. . 3 |- ( y = A -> ( E. x e. B y e. C <-> E. x e. B A e. C ) )
6		df-iun 4522	. . 3 |- U_ x e. B C = { y | E. x e. B y e. C }
7	5, 6	elab2g 3353	. 2 |- ( A e. _V -> ( A e. U_ x e. B C <-> E. x e. B A e. C ) )
8	1, 3, 7	pm5.21nii 368	1 |- ( A e. U_ x e. B C <-> E. x e. B A e. C )

Syntax hints:   <-> wb 196   = wceq 1483   e. wcel 1990   E.wrex 2913   _Vcvv 3200   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-iun 4522

This theorem is referenced by:  eliuni  4526  iuncom  4527  iuncom4  4528  iunconst  4529  iuniin  4531  iunss1  4532  ss2iun  4536  dfiun2g  4552  ssiun  4562  ssiun2  4563  iunab  4566  iun0  4576  0iun  4577  iunn0  4580  iunin2  4584  iundif2  4587  iindif2  4589  iunxsng  4602  iunun  4604  iunxun  4605  iunxdif3  4606  iunxiun  4608  iunpwss  4618  disjiun  4640  disjiund  4643  disjxiun  4649  disjxiunOLD  4650  triun  4766  otiunsndisj  4980  xpiundi  5173  xpiundir  5174  iunxpf  5270  cnvuni  5309  dmiun  5333  dmuni  5334  rniun  5543  xpdifid  5562  dfco2  5634  dfco2a  5635  coiun  5645  imaiun  6503  eluniima  6508  iunpw  6978  fun11iun  7126  opabex3d  7145  opabex3  7146  wfrdmcl  7423  onoviun  7440  smoiun  7458  oalimcl  7640  oaass  7641  oarec  7642  omordlim  7657  omlimcl  7658  omeulem1  7662  oelimcl  7680  oeeulem  7681  oaabs2  7725  omabs  7727  dffi3  8337  ixpiunwdom  8496  trcl  8604  r1ordg  8641  r1pwss  8647  rankr1ai  8661  r1elss  8669  fseqenlem2  8848  infpwfien  8885  cardaleph  8912  ackbij2  9065  cfsmolem  9092  alephsing  9098  hsmexlem2  9249  ac6c4  9303  ttukeylem6  9336  iunfo  9361  iundom2g  9362  konigthlem  9390  alephreg  9404  pwcfsdom  9405  pwfseqlem3  9482  inar1  9597  inatsk  9600  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  wrdval  13308  s3iunsndisj  13707  dfrtrclrec2  13797  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fsumiun  14553  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  prmreclem5  15624  imasaddfnlem  16188  imasvscafn  16197  efgsfo  18152  frgpnabllem1  18276  lssats2  19000  lbsextlem2  19159  lbsextlem3  19160  islpidl  19246  iunocv  20025  iunconnlem  21230  iunconn  21231  locfincmp  21329  alexsubALTlem3  21853  ptcmplem3  21858  imasdsf1olem  22178  zcld  22616  ovolfioo  23236  ovolficc  23237  ovoliunlem2  23271  ovoliunnul  23275  volfiniun  23315  iundisj  23316  iunmbl2  23325  volsup2  23373  vitalilem2  23378  ismbf3d  23421  mbfaddlem  23427  mbfsup  23431  i1faddlem  23460  i1fmullem  23461  elaa  24071  numedglnl  26039  clwwlksnun  26974  fusgreg2wsp  27200  iunin1f  29374  iunxsngf  29375  ssiun3  29376  iinssiun  29377  iunpreima  29383  iundisjf  29402  unipreima  29446  aciunf1lem  29462  ofpreima  29465  iundisjfi  29555  fsumiunle  29575  locfinreflem  29907  esum2dlem  30154  esum2d  30155  esumiun  30156  eulerpartlemgh  30440  dstfrvunirn  30536  reprsuc  30693  reprdifc  30705  bnj1405  30907  bnj916  31003  bnj983  31021  bnj1398  31102  bnj1417  31109  bnj1498  31129  mclsppslem  31480  eltrpred  31726  dftrpred3g  31733  trpredrec  31738  frrlem5e  31788  colinearex  32167  neibastop2lem  32355  rabiun  33382  iundif1  33383  volsupnfl  33454  istotbnd3  33570  sstotbnd  33574  sstotbnd3  33575  prdstotbnd  33593  cntotbnd  33595  heiborlem3  33612  heibor  33620  pclfinN  35186  pclcmpatN  35187  lcfrvalsnN  36830  lcfrlem5  36835  lcfrlem6  36836  lcfrlem16  36847  lcfrlem27  36858  lcfrlem37  36868  lcfr  36874  mapdrvallem2  36934  cnviun  37942  imaiun1  37943  coiun1  37944  ss2iundf  37951  eliunov2  37971  iunconnlem2  39171  iunxsngf2  39230  iunincfi  39272  eliuniin  39279  eliuniin2  39303  eliunid  39342  unirnmap  39400  unirnmapsn  39406  ssmapsn  39408  iunmapsn  39409  iuneqfzuzlem  39550  allbutfi  39616  fsumiunss  39807  fnlimfvre  39906  cnrefiisplem  40055  dvnprodlem1  40161  dvnprodlem2  40162  fourierdlem80  40403  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  iundjiun  40677  meaiininclem  40700  hoicvr  40762  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem3  40811  hspmbllem2  40841  opnvonmbllem2  40847  iunhoiioolem  40889  smfaddlem1  40971  smflimlem2  40980  smfmullem4  41001  smflimmpt  41016  smflimsuplem7  41032  smflimsuplem8  41033  smflimsupmpt  41035  smfliminfmpt  41038  otiunsndisjX  41298  iccpartiun  41370  iunord  42422