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

Theorem elun 3644
Description: Expansion of membership in class union. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 7-Aug-1994.)
Assertion
Ref Expression
elun

Proof of Theorem elun
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . 3
3 elex 3118 . . 3
42, 3jaoi 379 . 2
5 eleq1 2529 . . . 4
6 eleq1 2529 . . . 4
75, 6orbi12d 709 . . 3
8 df-un 3480 . . 3
97, 8elab2g 3248 . 2
101, 4, 9pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  =wceq 1395  e.wcel 1818   cvv 3109  u.cun 3473
This theorem is referenced by:  uneqri  3645  uncom  3647  uneq1  3650  unass  3660  ssun1  3666  unss1  3672  ssequn1  3673  unss  3677  rexun  3683  ralunb  3684  indi  3743  undi  3744  unineq  3747  undif3  3758  symdif2  3763  rabun2  3776  reuun2  3780  undif4  3883  ssundif  3911  dfpr2  4044  elpwunsn  4070  eltpg  4071  pwpr  4245  pwtp  4246  uniun  4268  intun  4319  iinun2  4396  iunun  4411  iunxun  4412  iinuni  4414  brun  4500  pwunss  4790  pwssun  4791  elsuci  4949  elsucg  4950  elsuc2g  4951  opthprc  5052  xpundi  5057  xpundir  5058  difxp  5436  sossfld  5459  funun  5635  mptun  5717  unpreima  6013  suceloni  6648  ordsucun  6660  fnse  6917  reldmtpos  6982  dftpos4  6993  tpostpos  6994  oarec  7230  brdom2  7565  unxpdomlem3  7746  domunfican  7813  dfsup2  7922  dfsup2OLD  7923  wemapso2OLD  7998  wemapso2lem  7999  unwdomg  8031  unxpwdom2  8035  sucprcregOLD  8047  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  rankunb  8289  iscard3  8495  kmlem2  8552  ssfin4  8711  dffin7-2  8799  fin1a2lem11  8811  fin1a2lem12  8812  cfpwsdom  8980  elgch  9021  fpwwe2lem13  9041  canthp1lem2  9052  gch2  9074  elnn0  10822  un0addcl  10854  un0mulcl  10855  ltxr  11353  elxr  11354  xrsupexmnf  11525  xrinfmexpnf  11526  supxrun  11536  ixxun  11574  difreicc  11681  iccsplit  11682  fzsplit2  11739  elfzp1  11759  uzsplit  11779  elfzp12  11786  fzosplit  11858  fzouzsplit  11860  elfzonlteqm1  11891  fzosplitsni  11920  hashnn0pnf  12415  hashf1lem2  12505  hash2pwpr  12519  pr2pwpr  12520  ccatrn  12606  cats1un  12701  fsumsplit  13562  sumsplit  13583  fprodsplit  13770  rpnnen2  13959  saddisjlem  14114  nnnn0modprm0  14331  vdwapun  14492  ramubcl  14536  xpsfrnel2  14962  mreexmrid  15040  lubun  15753  symgextf1  16446  gsumzsplit  16944  gsumzsplitOLD  16945  gsumzunsnd  16982  gsumunsnfd  16983  dprddisj2  17087  dprddisj2OLD  17088  dmdprdsplit2lem  17094  dmdprdsplit2  17095  dprdsplit  17097  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem4OLD  18173  evlslem4  18174  mdetunilem9  19122  maducoeval2  19142  madugsum  19145  clslp  19649  islpi  19650  restntr  19683  pnfnei  19721  mnfnei  19722  iuncon  19929  refun0  20016  xkoptsub  20155  ptunhmeo  20309  fbun  20341  filcon  20384  fixufil  20423  ufildr  20432  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  tsmssplit  20654  xrtgioo  21311  reconnlem2  21332  iccpnfcnv  21444  iccpnfhmeo  21445  rrxcph  21824  rrxdstprj1  21836  mbfss  22053  mbfmax  22056  itg2splitlem  22155  itg2split  22156  iblss2  22212  itgsplit  22242  limcdif  22280  ellimc2  22281  limcmpt  22287  limcres  22290  limccnp  22295  limccnp2  22296  limcco  22297  rollelem  22390  dvivthlem1  22409  dvne0  22412  lhop  22417  degltlem1  22472  ply1rem  22564  fta1glem2  22567  plypf1  22609  plyaddlem1  22610  plymullem1  22611  plycj  22674  ofmulrt  22678  taylfval  22754  abelthlem2  22827  abelthlem3  22828  reasinsin  23227  scvxcvx  23315  ppinprm  23426  chtnprm  23428  dchrfi  23530  lgsdir2  23603  usgraexmpl  24401  vdgrf  24898  vdgrun  24901  vdgrfiun  24902  vdgfrgragt2  25027  frgrawopreglem2  25045  shunssi  26286  atomli  27301  atoml2i  27302  isoun  27520  fzsplit3  27599  eliccioo  27627  ordtconlem1  27906  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  esumsplit  28063  measvuni  28185  sxbrsigalem0  28242  subfacp1lem4  28627  subfacp1lem5  28628  kur14lem7  28656  mrsubcv  28870  mclsax  28929  dftrpred3g  29316  wfrlem14  29356  wfrlem15  29357  elsymdif  29473  brcup  29589  tan2h  30047  ftc1anclem1  30090  ftc1anclem5  30094  dvasin  30103  dvacos  30104  refssfne  30176  eqfnun  30212  smprngopr  30449  lzunuz  30701  jm2.23  30938  unxpwdom3  31041  hbtlem5  31077  radcnvrat  31195  bccbc  31250  fnchoice  31404  elunnel1  31414  elunnel2  31415  unima  31441  limciccioolb  31627  limcicciooub  31643  icccncfext  31690  cncfiooicclem1  31696  fourierdlem70  31959  fourierdlem80  31969  fourierdlem93  31982  fourierdlem101  31990  undif3VD  33682  iunconlem2  33735  bnj1138  33847  bnj1137  34051  bj-eltag  34535  bj-0eltag  34536  bj-sngltag  34541  bj-projun  34552  elpadd  35523  paddval0  35534  hdmaplem4  37501  mapdh9a  37517  rp-fakeinunass  37740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480
  Copyright terms: Public domain W3C validator