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

Theorem eliun 4655
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.
StepHypRef Expression
1 elex 3360 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3360 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3175 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2836 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3198 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4653 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3501 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 367 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1629  wcel 2143  wrex 3060  Vcvv 3348   ciun 4651
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064  df-rex 3065  df-v 3350  df-iun 4653
This theorem is referenced by:  eliuni  4657  iuncom  4658  iuncom4  4659  iunconst  4660  iuniin  4662  iunss1  4663  ss2iun  4667  dfiun2g  4683  ssiun  4693  ssiun2  4694  iunab  4697  iun0  4707  0iun  4708  iunn0  4711  iunin2  4715  iundif2  4718  iindif2  4720  iunxsng  4733  iunun  4735  iunxun  4736  iunxdif3  4737  iunxiun  4739  iunpwss  4749  disjiun  4771  disjiund  4774  disjxiun  4780  triun  4896  otiunsndisj  5112  xpiundi  5312  xpiundir  5313  iunxpf  5408  cnvuni  5446  dmiun  5470  dmuni  5471  rniun  5683  xpdifid  5702  dfco2  5777  dfco2a  5778  coiun  5788  imaiun  6644  eluniima  6649  iunpw  7123  fun11iun  7271  opabex3d  7290  opabex3  7291  wfrdmcl  7574  onoviun  7591  smoiun  7609  oalimcl  7792  oaass  7793  oarec  7794  omordlim  7809  omlimcl  7810  omeulem1  7814  oelimcl  7832  oeeulem  7833  oaabs2  7877  omabs  7879  dffi3  8491  ixpiunwdom  8650  trcl  8766  r1ordg  8803  r1pwss  8809  rankr1ai  8823  r1elss  8831  fseqenlem2  9046  infpwfien  9083  cardaleph  9110  ackbij2  9265  cfsmolem  9292  alephsing  9298  hsmexlem2  9449  ac6c4  9503  ttukeylem6  9536  iunfo  9561  iundom2g  9562  konigthlem  9590  alephreg  9604  pwcfsdom  9605  pwfseqlem3  9682  inar1  9797  inatsk  9800  fsuppmapnn0fiub  12997  fsuppmapnn0fiubOLD  12998  wrdval  13507  s3iunsndisj  13920  dfrtrclrec2  14008  fsum2dlem  14712  fsumcom2  14716  fsumcom2OLD  14717  fsumiun  14764  fprod2dlem  14921  fprodcom2  14925  fprodcom2OLD  14926  prmreclem5  15837  imasaddfnlem  16402  imasvscafn  16411  efgsfo  18365  frgpnabllem1  18489  lssats2  19219  lbsextlem2  19380  lbsextlem3  19381  islpidl  19467  iunocv  20248  iunconnlem  21457  iunconn  21458  locfincmp  21556  alexsubALTlem3  22079  ptcmplem3  22084  imasdsf1olem  22404  zcld  22842  ovolfioo  23461  ovolficc  23462  ovoliunlem2  23497  ovoliunnul  23501  volfiniun  23541  iundisj  23542  iunmbl2  23551  volsup2  23599  vitalilem2  23603  ismbf3d  23647  mbfaddlem  23653  mbfsup  23657  i1faddlem  23686  i1fmullem  23687  elaa  24297  numedglnl  26267  clwwlknun  27292  clwwlknunOLD  27297  fusgreg2wsp  27522  iunin1f  29713  iunxsngf  29714  ssiun3  29715  iinssiun  29716  iunpreima  29722  iundisjf  29741  unipreima  29787  aciunf1lem  29803  ofpreima  29806  iundisjfi  29896  fsumiunle  29916  locfinreflem  30248  esum2dlem  30495  esum2d  30496  esumiun  30497  eulerpartlemgh  30781  dstfrvunirn  30877  reprsuc  31034  reprdifc  31046  bnj1405  31246  bnj916  31342  bnj983  31360  bnj1398  31441  bnj1417  31448  bnj1498  31468  mclsppslem  31819  eltrpred  32063  dftrpred3g  32070  trpredrec  32075  frrlem5e  32126  colinearex  32505  neibastop2lem  32693  rabiun  33715  iundif1  33716  volsupnfl  33787  istotbnd3  33902  sstotbnd  33906  sstotbnd3  33907  prdstotbnd  33925  cntotbnd  33927  heiborlem3  33944  heibor  33952  pclfinN  35708  pclcmpatN  35709  lcfrvalsnN  37351  lcfrlem5  37356  lcfrlem6  37357  lcfrlem16  37368  lcfrlem27  37379  lcfrlem37  37389  lcfr  37395  mapdrvallem2  37455  cnviun  38468  imaiun1  38469  coiun1  38470  ss2iundf  38477  eliunov2  38497  iunconnlem2  39694  iunxsngf2  39752  iunincfi  39794  eliuniin  39801  eliuniin2  39825  eliunid  39863  unirnmap  39919  unirnmapsn  39925  ssmapsn  39927  iunmapsn  39928  iuneqfzuzlem  40067  allbutfi  40133  fsumiunss  40326  fnlimfvre  40425  cnrefiisplem  40574  dvnprodlem1  40680  dvnprodlem2  40681  fourierdlem80  40921  sge0iunmptlemfi  41148  sge0iunmptlemre  41150  sge0iunmpt  41153  iundjiun  41195  meaiininclem  41221  hoicvr  41283  hoidmv1lelem3  41328  hoidmv1le  41329  hoidmvlelem3  41332  hspmbllem2  41362  opnvonmbllem2  41368  iunhoiioolem  41410  smfaddlem1  41492  smflimlem2  41501  smfmullem4  41522  smflimmpt  41537  smflimsuplem7  41553  smflimsuplem8  41554  smflimsupmpt  41556  smfliminfmpt  41559  otiunsndisjX  41821  iccpartiun  41895  iunord  42947
  Copyright terms: Public domain W3C validator