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

Theorem eluni 4252
Description: Membership in class union. (Contributed by NM, 22-May-1994.)
Assertion
Ref Expression
eluni
Distinct variable groups:   ,   ,

Proof of Theorem eluni
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . . 4
32adantr 465 . . 3
43exlimiv 1722 . 2
5 eleq1 2529 . . . . 5
65anbi1d 704 . . . 4
76exbidv 1714 . . 3
8 df-uni 4250 . . 3
97, 8elab2g 3248 . 2
101, 4, 9pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109  U.cuni 4249
This theorem is referenced by:  eluni2  4253  elunii  4254  eluniab  4260  uniun  4268  uniin  4269  uniss  4270  unissb  4281  dftr2  4547  unipw  4702  dmuni  5217  fununi  5659  elunirn  6163  uniex2  6595  uniuni  6609  mpt2xopxnop0  6962  tfrlem7  7071  tfrlem9a  7074  inf2  8061  inf3lem2  8067  rankwflemb  8232  cardprclem  8381  carduni  8383  iunfictbso  8516  kmlem3  8553  kmlem4  8554  cfub  8650  isf34lem4  8778  grothtsk  9234  suplem1pr  9451  isbasis2g  19449  tgval2  19457  ntreq0  19578  cmpsublem  19899  cmpsub  19900  cmpcld  19902  is1stc2  19943  alexsubALTlem3  20549  alexsubALT  20551  wfrlem11  29353  frrlem5c  29393  fnessref  30175  elunif  31391  ssfiunibd  31509  stoweidlem27  31809  stoweidlem48  31830  truniALT  33312  truniALTVD  33678  unisnALT  33726
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-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-uni 4250
  Copyright terms: Public domain W3C validator