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

Theorem elun2 3977
Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
elun2 (𝐴𝐵𝐴 ∈ (𝐶𝐵))

Proof of Theorem elun2
StepHypRef Expression
1 ssun2 3973 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3791 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2158  cun 3764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-v 3392  df-un 3771  df-in 3773  df-ss 3780
This theorem is referenced by:  dftpos4  7603  wfrlem14  7661  tfrlem11  7717  findcard2d  8438  cantnfp1lem1  8819  cantnfp1lem3  8821  tc2  8862  rankunb  8957  rankelun  8979  djurcl  9017  djuss  9026  djuun  9032  dfac2b  9233  dfac2OLD  9235  cfsmolem  9374  isfin4-3  9419  zornn0g  9609  mnfxr  10378  supxrun  12360  fsumsplitsnun  14703  fsumsplitsnunOLD  14705  sumsplit  14718  modfsummodslem1  14742  prmreclem5  15837  acsfiindd  17378  lspsolv  19347  mplcoe1  19670  maducoeval2  20653  restntr  21196  1stckgenlem  21566  fbun  21853  filuni  21898  ufileu  21932  alexsubALTlem4  22063  tmdgsum  22108  icccmplem2  22835  aannenlem2  24294  aalioulem2  24298  ebtwntg  26072  elntg  26074  bnj553  31288  bnj966  31334  bnj1442  31437  mrsubrn  31730  elmrsubrn  31737  mvhf  31775  msubvrs  31777  altxpsspw  32402  matunitlindflem1  33715  poimirlem3  33722  poimirlem31  33750  poimirlem32  33751  mbfresfi  33765  itg2addnclem2  33771  ftc1anclem7  33800  ftc1anc  33802  hdmaplem2N  37550  hdmaplem3  37551  sucidVD  39599  mccllem  40306  limcresiooub  40351  limcresioolb  40352  cnrefiisplem  40532  dvmptfprodlem  40636  dvmptfprod  40637  dvnprodlem1  40638  dvnprodlem2  40639  fourierdlem20  40820  fourierdlem38  40838  fourierdlem48  40847  fourierdlem49  40848  fourierdlem51  40850  fourierdlem62  40861  fourierdlem63  40862  fourierdlem64  40863  fourierdlem65  40864  fourierdlem71  40870  fouriersw  40924  nnfoctbdjlem  41148  isomenndlem  41223  hoiprodp1  41281  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem3  41290  hoidmvlelem4  41291  hspmbllem2  41320  pimrecltpos  41398  setsidel  41918
  Copyright terms: Public domain W3C validator