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

Theorem eliun 4682
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 3365 . 2 (𝐴 𝑥𝐵 𝐶𝐴 ∈ V)
2 elex 3365 . . 3 (𝐴𝐶𝐴 ∈ V)
32rexlimivw 3176 . 2 (∃𝑥𝐵 𝐴𝐶𝐴 ∈ V)
4 eleq1 2832 . . . 4 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
54rexbidv 3199 . . 3 (𝑦 = 𝐴 → (∃𝑥𝐵 𝑦𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
6 df-iun 4680 . . 3 𝑥𝐵 𝐶 = {𝑦 ∣ ∃𝑥𝐵 𝑦𝐶}
75, 6elab2g 3510 . 2 (𝐴 ∈ V → (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶))
81, 3, 7pm5.21nii 369 1 (𝐴 𝑥𝐵 𝐶 ↔ ∃𝑥𝐵 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1652  wcel 2155  wrex 3056  Vcvv 3350   ciun 4678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-v 3352  df-iun 4680
This theorem is referenced by:  eliuni  4684  iuncom  4685  iuncom4  4686  iunconst  4687  iuniin  4689  iunss1  4690  ss2iun  4694  dfiun2g  4710  ssiun  4720  ssiun2  4721  iunab  4724  iun0  4734  0iun  4735  iunn0  4738  iunin2  4742  iundif2  4745  iindif2  4747  iunxsng  4760  iunxsngf  4762  iunun  4763  iunxun  4764  iunxdif3  4765  iunxiun  4767  iunpwss  4777  disjiun  4799  disjiund  4802  disjxiun  4808  triun  4926  otiunsndisj  5143  xpiundi  5343  xpiundir  5344  iunxpf  5441  cnvuni  5479  dmiun  5503  dmuni  5504  rniun  5728  xpdifid  5747  dfco2  5822  dfco2a  5823  coiun  5833  imaiun  6697  eluniima  6702  iunpw  7178  fun11iun  7326  opabex3d  7345  opabex3  7346  wfrdmcl  7629  onoviun  7646  smoiun  7664  oalimcl  7847  oaass  7848  oarec  7849  omordlim  7864  omlimcl  7865  omeulem1  7869  oelimcl  7887  oeeulem  7888  oaabs2  7932  omabs  7934  dffi3  8546  ixpiunwdom  8705  trcl  8821  r1ordg  8858  r1pwss  8864  rankr1ai  8878  r1elss  8886  fseqenlem2  9101  infpwfien  9138  cardaleph  9165  ackbij2  9320  cfsmolem  9347  alephsing  9353  hsmexlem2  9504  ac6c4  9558  ttukeylem6  9591  iunfo  9616  iundom2g  9617  konigthlem  9645  alephreg  9659  pwcfsdom  9660  pwfseqlem3  9737  inar1  9852  inatsk  9855  fsuppmapnn0fiub  13001  wrdval  13492  s3iunsndisj  13997  dfrtrclrec2  14085  fsum2dlem  14789  fsumcom2  14793  fsumiun  14840  fprod2dlem  14996  fprodcom2  15000  prmreclem5  15906  imasaddfnlem  16457  imasvscafn  16466  efgsfo  18420  frgpnabllem1  18545  lssats2  19275  lbsextlem2  19436  lbsextlem3  19437  islpidl  19523  iunocv  20304  iunconnlem  21513  iunconn  21514  locfincmp  21612  alexsubALTlem3  22135  ptcmplem3  22140  imasdsf1olem  22460  zcld  22898  ovolfioo  23528  ovolficc  23529  ovoliunlem2  23564  ovoliunnul  23568  volfiniun  23608  iundisj  23609  iunmbl2  23618  volsup2  23666  vitalilem2  23670  ismbf3d  23715  mbfaddlem  23721  mbfsup  23725  i1faddlem  23754  i1fmullem  23755  elaa  24365  numedglnl  26320  clwwlknun  27389  clwwlknunOLD  27394  fusgreg2wsp  27619  iunin1f  29826  ssiun3  29827  iinssiun  29828  iunpreima  29834  iundisjf  29853  unipreima  29899  aciunf1lem  29915  ofpreima  29918  iundisjfi  30007  fsumiunle  30027  locfinreflem  30357  esum2dlem  30604  esum2d  30605  esumiun  30606  eulerpartlemgh  30890  dstfrvunirn  30987  reprsuc  31147  reprdifc  31159  bnj1405  31358  bnj916  31454  bnj983  31472  bnj1398  31553  bnj1417  31560  bnj1498  31580  mclsppslem  31931  eltrpred  32172  dftrpred3g  32179  trpredrec  32184  frrlem5e  32235  colinearex  32614  neibastop2lem  32801  rabiun  33809  iundif1  33810  volsupnfl  33881  istotbnd3  33995  sstotbnd  33999  sstotbnd3  34000  prdstotbnd  34018  cntotbnd  34020  heiborlem3  34037  heibor  34045  pclfinN  35859  pclcmpatN  35860  lcfrvalsnN  37500  lcfrlem5  37505  lcfrlem6  37506  lcfrlem16  37517  lcfrlem27  37528  lcfrlem37  37538  lcfr  37544  mapdrvallem2  37604  cnviun  38620  imaiun1  38621  coiun1  38622  ss2iundf  38629  eliunov2  38649  iunconnlem2  39826  iunxsngf2  39884  iunincfi  39926  eliuniin  39933  eliuniin2  39956  eliunid  39992  unirnmap  40048  unirnmapsn  40054  ssmapsn  40056  iunmapsn  40057  iuneqfzuzlem  40191  allbutfi  40256  fsumiunss  40448  fnlimfvre  40547  cnrefiisplem  40696  dvnprodlem1  40802  dvnprodlem2  40803  fourierdlem80  41043  sge0iunmptlemfi  41270  sge0iunmptlemre  41272  sge0iunmpt  41275  iundjiun  41317  meaiininclem  41343  hoicvr  41405  hoidmv1lelem3  41450  hoidmv1le  41451  hoidmvlelem3  41454  hspmbllem2  41484  opnvonmbllem2  41490  iunhoiioolem  41532  smfaddlem1  41614  smflimlem2  41623  smfmullem4  41644  smflimmpt  41659  smflimsuplem7  41675  smflimsuplem8  41676  smflimsupmpt  41678  smfliminfmpt  41681  otiunsndisjX  42031  iccpartiun  42107  iunord  43094
  Copyright terms: Public domain W3C validator