MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eliun Unicode version

Theorem eliun 4057
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.
StepHypRef Expression
1 elex 2924 . 2  |-  ( A  e.  U_ x  e.  B  C  ->  A  e.  _V )
2 elex 2924 . . 3  |-  ( A  e.  C  ->  A  e.  _V )
32rexlimivw 2786 . 2  |-  ( E. x  e.  B  A  e.  C  ->  A  e. 
_V )
4 eleq1 2464 . . . 4  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
54rexbidv 2687 . . 3  |-  ( y  =  A  ->  ( E. x  e.  B  y  e.  C  <->  E. x  e.  B  A  e.  C ) )
6 df-iun 4055 . . 3  |-  U_ x  e.  B  C  =  { y  |  E. x  e.  B  y  e.  C }
75, 6elab2g 3044 . 2  |-  ( A  e.  _V  ->  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C ) )
81, 3, 7pm5.21nii 343 1  |-  ( A  e.  U_ x  e.  B  C  <->  E. x  e.  B  A  e.  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    e. wcel 1721   E.wrex 2667   _Vcvv 2916   U_ciun 4053
This theorem is referenced by:  iuncom  4059  iuncom4  4060  iunconst  4061  iuniin  4063  iunss1  4064  ss2iun  4068  dfiun2g  4083  ssiun  4093  ssiun2  4094  iunab  4097  iun0  4107  0iun  4108  iunn0  4111  iunin2  4115  iundif2  4118  iindif2  4120  iunxsng  4129  iunun  4131  iunxun  4132  iunxiun  4133  iunpwss  4140  disjiun  4162  disjxiun  4169  triun  4275  iunpw  4718  xpiundi  4891  xpiundir  4892  iunxpf  4980  cnvuni  5016  dmiun  5037  dmuni  5038  rniun  5241  dfco2  5328  dfco2a  5329  coiun  5338  fun11iun  5654  opabex3d  5948  opabex3  5949  imaiun  5951  eluniima  5956  onoviun  6564  smoiun  6582  oalimcl  6762  oaass  6763  oarec  6764  omordlim  6779  omlimcl  6780  omeulem1  6784  oeordi  6789  oelimcl  6802  oeeulem  6803  oaabs2  6847  omabs  6849  dffi3  7394  ixpiunwdom  7515  trcl  7620  r1ordg  7660  r1pwss  7666  rankr1ai  7680  r1elss  7688  fseqenlem2  7862  fseqdom  7863  infpwfien  7899  cardaleph  7926  ackbij2  8079  cfsmolem  8106  alephsing  8112  hsmexlem2  8263  axdc3lem2  8287  ac6c4  8317  ttukeylem6  8350  iunfo  8370  iundom2g  8371  konigthlem  8399  alephreg  8413  pwcfsdom  8414  pwfseqlem3  8491  inar1  8606  inatsk  8609  wrdval  11685  fsum2dlem  12509  fsumcom2  12513  fsumiun  12555  prmreclem5  13243  imasaddfnlem  13708  imasvscafn  13717  efgs1b  15323  efgsfo  15326  frgpnabllem1  15439  lssats2  16031  lbsextlem2  16186  lbsextlem3  16187  islpidl  16272  iunocv  16863  iunconlem  17443  iuncon  17444  alexsubALTlem3  18033  ptcmplem3  18038  imasdsf1olem  18356  zcld  18797  ovolfioo  19317  ovolficc  19318  ovoliunlem2  19352  ovoliunnul  19356  volfiniun  19394  iundisj  19395  iunmbl2  19404  volsup2  19450  vitalilem2  19454  ismbf3d  19499  mbfaddlem  19505  mbfsup  19509  i1faddlem  19538  i1fmullem  19539  elaa  20186  ssiun3  23962  iundisjf  23982  unipreima  24009  ofpreima  24034  iundisjfi  24105  dstfrvunirn  24685  dfrtrclrec2  25096  fprod2dlem  25257  fprodcom2  25261  eltrpred  25443  dftrpred3g  25450  trpredrec  25455  wfrlem9  25478  frrlem5e  25503  nofulllem5  25574  colinearex  25898  rabiun2  26139  volsupnfl  26150  locfincmp  26274  neibastop2lem  26279  istotbnd3  26370  sstotbnd  26374  sstotbnd3  26375  prdstotbnd  26393  cntotbnd  26395  heiborlem3  26412  heibor  26420  otiunsndisj  27954  otiunsndisjX  27955  2spotiundisj  28165  usgreg2spot  28170  bnj1405  28914  bnj916  29010  bnj983  29028  bnj1398  29109  bnj1417  29116  bnj1498  29136  pclfinN  30382  pclcmpatN  30383  lcfrvalsnN  32024  lcfrlem5  32029  lcfrlem6  32030  lcfrlem16  32041  lcfrlem27  32052  lcfrlem37  32062  lcfr  32068  mapdrvallem2  32128
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-v 2918  df-iun 4055
  Copyright terms: Public domain W3C validator