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

Theorem elun2 4107
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 4103 . 2 𝐵 ⊆ (𝐶𝐵)
21sseli 3914 1 (𝐴𝐵𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  cun 3882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901
This theorem is referenced by:  dftpos4  7898  wfrlem14  7955  tfrlem11  8011  findcard2d  8748  cantnfp1lem1  9129  cantnfp1lem3  9131  tc2  9172  rankunb  9267  rankelun  9289  djurcl  9328  djuss  9337  djuun  9343  dfac2b  9545  cfsmolem  9685  isfin4p1  9730  zornn0g  9920  mnfxr  10691  supxrun  12701  fsumsplitsnun  15105  sumsplit  15118  modfsummodslem1  15142  prmreclem5  16249  acsfiindd  17782  lspsolv  19911  mplcoe1  20708  maducoeval2  21248  restntr  21790  1stckgenlem  22161  fbun  22448  filuni  22493  ufileu  22527  alexsubALTlem4  22658  tmdgsum  22703  icccmplem2  23431  aannenlem2  24928  aalioulem2  24932  ebtwntg  26779  elntg  26781  bnj553  32278  bnj966  32324  bnj1442  32429  srcmpltd  32454  mrsubrn  32868  elmrsubrn  32875  mvhf  32913  msubvrs  32915  altxpsspw  33546  exrecfnlem  34791  matunitlindflem1  35046  poimirlem3  35053  poimirlem31  35081  poimirlem32  35082  mbfresfi  35096  itg2addnclem2  35102  ftc1anclem7  35129  ftc1anc  35131  hdmaplem2N  39061  hdmaplem3  39062  metakunt22  39362  sucidVD  41565  mccllem  42226  limcresiooub  42271  limcresioolb  42272  cnrefiisplem  42458  dvmptfprodlem  42573  dvmptfprod  42574  dvnprodlem1  42575  dvnprodlem2  42576  fourierdlem20  42756  fourierdlem38  42774  fourierdlem48  42783  fourierdlem49  42784  fourierdlem51  42786  fourierdlem62  42797  fourierdlem63  42798  fourierdlem64  42799  fourierdlem65  42800  fourierdlem71  42806  fouriersw  42860  nnfoctbdjlem  43081  isomenndlem  43156  hoiprodp1  43214  hoidmvlelem1  43221  hoidmvlelem2  43222  hoidmvlelem3  43223  hoidmvlelem4  43224  hspmbllem2  43253  pimrecltpos  43331  setsidel  43880
  Copyright terms: Public domain W3C validator