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

Theorem elun2 3925
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 3921 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3741 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2140  cun 3714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730
This theorem is referenced by:  dftpos4  7542  wfrlem14  7599  tfrlem11  7655  findcard2d  8370  cantnfp1lem1  8751  cantnfp1lem3  8753  tc2  8794  rankunb  8889  rankelun  8911  djurcl  8949  djuss  8958  djuun  8963  dfac2b  9164  dfac2OLD  9166  cfsmolem  9305  isfin4-3  9350  zornn0g  9540  mnfxr  10309  supxrun  12360  fsumsplitsnun  14704  fsumsplitsnunOLD  14706  sumsplit  14719  modfsummodslem1  14744  prmreclem5  15847  acsfiindd  17399  lspsolv  19366  mplcoe1  19688  maducoeval2  20669  restntr  21209  1stckgenlem  21579  fbun  21866  filuni  21911  ufileu  21945  alexsubALTlem4  22076  tmdgsum  22121  icccmplem2  22848  aannenlem2  24304  aalioulem2  24308  ebtwntg  26083  elntg  26085  bnj553  31297  bnj966  31343  bnj1442  31446  mrsubrn  31739  elmrsubrn  31746  mvhf  31784  msubvrs  31786  altxpsspw  32412  matunitlindflem1  33737  poimirlem3  33744  poimirlem31  33772  poimirlem32  33773  mbfresfi  33788  itg2addnclem2  33794  ftc1anclem7  33823  ftc1anc  33825  hdmaplem2N  37582  hdmaplem3  37583  sucidVD  39626  mccllem  40351  limcresiooub  40396  limcresioolb  40397  cnrefiisplem  40577  dvmptfprodlem  40681  dvmptfprod  40682  dvnprodlem1  40683  dvnprodlem2  40684  fourierdlem20  40866  fourierdlem38  40884  fourierdlem48  40893  fourierdlem49  40894  fourierdlem51  40896  fourierdlem62  40907  fourierdlem63  40908  fourierdlem64  40909  fourierdlem65  40910  fourierdlem71  40916  fouriersw  40970  nnfoctbdjlem  41194  isomenndlem  41269  hoiprodp1  41327  hoidmvlelem1  41334  hoidmvlelem2  41335  hoidmvlelem3  41336  hoidmvlelem4  41337  hspmbllem2  41366  pimrecltpos  41444  setsidel  41875
  Copyright terms: Public domain W3C validator