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

Theorem elun2 4150
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 4146 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3960 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cun 3931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949
This theorem is referenced by:  dftpos4  7900  wfrlem14  7957  tfrlem11  8013  findcard2d  8748  cantnfp1lem1  9129  cantnfp1lem3  9131  tc2  9172  rankunb  9267  rankelun  9289  djurcl  9328  djuss  9337  djuun  9343  dfac2b  9544  cfsmolem  9680  isfin4p1  9725  zornn0g  9915  mnfxr  10686  supxrun  12697  fsumsplitsnun  15098  sumsplit  15111  modfsummodslem1  15135  prmreclem5  16244  acsfiindd  17775  lspsolv  19844  mplcoe1  20174  maducoeval2  21177  restntr  21718  1stckgenlem  22089  fbun  22376  filuni  22421  ufileu  22455  alexsubALTlem4  22586  tmdgsum  22631  icccmplem2  23358  aannenlem2  24845  aalioulem2  24849  ebtwntg  26695  elntg  26697  bnj553  32069  bnj966  32115  bnj1442  32218  srcmpltd  32243  mrsubrn  32657  elmrsubrn  32664  mvhf  32702  msubvrs  32704  altxpsspw  33335  exrecfnlem  34542  matunitlindflem1  34769  poimirlem3  34776  poimirlem31  34804  poimirlem32  34805  mbfresfi  34819  itg2addnclem2  34825  ftc1anclem7  34854  ftc1anc  34856  hdmaplem2N  38788  hdmaplem3  38789  sucidVD  41083  mccllem  41754  limcresiooub  41799  limcresioolb  41800  cnrefiisplem  41986  dvmptfprodlem  42105  dvmptfprod  42106  dvnprodlem1  42107  dvnprodlem2  42108  fourierdlem20  42289  fourierdlem38  42307  fourierdlem48  42316  fourierdlem49  42317  fourierdlem51  42319  fourierdlem62  42330  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem71  42339  fouriersw  42393  nnfoctbdjlem  42614  isomenndlem  42689  hoiprodp1  42747  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  hspmbllem2  42786  pimrecltpos  42864  setsidel  43413
  Copyright terms: Public domain W3C validator