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

Theorem eliun 4515
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 3207 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3207 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3025 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2687 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3048 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4513 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3347 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 368 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481  wcel 1988  wrex 2910  Vcvv 3195   ciun 4511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-v 3197  df-iun 4513
This theorem is referenced by:  eliuni  4517  iuncom  4518  iuncom4  4519  iunconst  4520  iuniin  4522  iunss1  4523  ss2iun  4527  dfiun2g  4543  ssiun  4553  ssiun2  4554  iunab  4557  iun0  4567  0iun  4568  iunn0  4571  iunin2  4575  iundif2  4578  iindif2  4580  iunxsng  4593  iunun  4595  iunxun  4596  iunxdif3  4597  iunxiun  4599  iunpwss  4609  disjiun  4631  disjiund  4634  disjxiun  4640  disjxiunOLD  4641  triun  4757  otiunsndisj  4970  xpiundi  5163  xpiundir  5164  iunxpf  5259  cnvuni  5298  dmiun  5322  dmuni  5323  rniun  5531  xpdifid  5550  dfco2  5622  dfco2a  5623  coiun  5633  imaiun  6488  eluniima  6493  iunpw  6963  fun11iun  7111  opabex3d  7130  opabex3  7131  wfrdmcl  7408  onoviun  7425  smoiun  7443  oalimcl  7625  oaass  7626  oarec  7627  omordlim  7642  omlimcl  7643  omeulem1  7647  oelimcl  7665  oeeulem  7666  oaabs2  7710  omabs  7712  dffi3  8322  ixpiunwdom  8481  trcl  8589  r1ordg  8626  r1pwss  8632  rankr1ai  8646  r1elss  8654  fseqenlem2  8833  infpwfien  8870  cardaleph  8897  ackbij2  9050  cfsmolem  9077  alephsing  9083  hsmexlem2  9234  ac6c4  9288  ttukeylem6  9321  iunfo  9346  iundom2g  9347  konigthlem  9375  alephreg  9389  pwcfsdom  9390  pwfseqlem3  9467  inar1  9582  inatsk  9585  fsuppmapnn0fiub  12773  fsuppmapnn0fiubOLD  12774  wrdval  13291  s3iunsndisj  13688  dfrtrclrec2  13778  fsum2dlem  14482  fsumcom2  14486  fsumcom2OLD  14487  fsumiun  14534  fprod2dlem  14691  fprodcom2  14695  fprodcom2OLD  14696  prmreclem5  15605  imasaddfnlem  16169  imasvscafn  16178  efgsfo  18133  frgpnabllem1  18257  lssats2  18981  lbsextlem2  19140  lbsextlem3  19141  islpidl  19227  iunocv  20006  iunconnlem  21211  iunconn  21212  locfincmp  21310  alexsubALTlem3  21834  ptcmplem3  21839  imasdsf1olem  22159  zcld  22597  ovolfioo  23217  ovolficc  23218  ovoliunlem2  23252  ovoliunnul  23256  volfiniun  23296  iundisj  23297  iunmbl2  23306  volsup2  23354  vitalilem2  23359  ismbf3d  23402  mbfaddlem  23408  mbfsup  23412  i1faddlem  23441  i1fmullem  23442  elaa  24052  numedglnl  26020  clwwlksnun  26954  fusgreg2wsp  27174  iunin1f  29346  iunxsngf  29347  ssiun3  29348  iinssiun  29349  iunpreima  29355  iundisjf  29374  unipreima  29419  aciunf1lem  29435  ofpreima  29439  iundisjfi  29529  fsumiunle  29549  locfinreflem  29881  esum2dlem  30128  esum2d  30129  esumiun  30130  eulerpartlemgh  30414  dstfrvunirn  30510  reprsuc  30667  reprdifc  30679  bnj1405  30881  bnj916  30977  bnj983  30995  bnj1398  31076  bnj1417  31083  bnj1498  31103  mclsppslem  31454  eltrpred  31700  dftrpred3g  31707  trpredrec  31712  frrlem5e  31762  colinearex  32142  neibastop2lem  32330  rabiun  33353  iundif1  33354  volsupnfl  33425  istotbnd3  33541  sstotbnd  33545  sstotbnd3  33546  prdstotbnd  33564  cntotbnd  33566  heiborlem3  33583  heibor  33591  pclfinN  35005  pclcmpatN  35006  lcfrvalsnN  36649  lcfrlem5  36654  lcfrlem6  36655  lcfrlem16  36666  lcfrlem27  36677  lcfrlem37  36687  lcfr  36693  mapdrvallem2  36753  cnviun  37761  imaiun1  37762  coiun1  37763  ss2iundf  37770  eliunov2  37790  iunconnlem2  38991  iunxsngf2  39050  iunincfi  39092  eliuniin  39099  eliuniin2  39123  unirnmap  39216  unirnmapsn  39222  ssmapsn  39224  iunmapsn  39225  iuneqfzuzlem  39363  allbutfi  39429  fsumiunss  39607  fnlimfvre  39706  dvnprodlem1  39924  dvnprodlem2  39925  fourierdlem80  40166  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  sge0iunmpt  40398  iundjiun  40440  meaiininclem  40463  hoicvr  40525  hoidmv1lelem3  40570  hoidmv1le  40571  hoidmvlelem3  40574  hspmbllem2  40604  opnvonmbllem2  40610  iunhoiioolem  40652  smfaddlem1  40734  smflimlem2  40743  smfmullem4  40764  smflimmpt  40779  smflimsuplem7  40795  smflimsuplem8  40796  smflimsupmpt  40798  smfliminfmpt  40801  otiunsndisjX  41061  iccpartiun  41134  iunord  42187
  Copyright terms: Public domain W3C validator