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

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

Proof of Theorem elun1
StepHypRef Expression
1 ssun1 3809 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3632 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cun 3605
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621
This theorem is referenced by:  brtpos  7406  dftpos4  7416  domunsncan  8101  unxpdomlem2  8206  rankunb  8751  rankelun  8773  fin1a2lem10  9269  zornn0g  9365  xrsupexmnf  12173  xrinfmexpnf  12174  sumsplit  14543  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  prmreclem5  15671  lbsextlem3  19208  restntr  21034  comppfsc  21383  1stckgenlem  21404  fbun  21691  filconn  21734  filuni  21736  alexsubALTlem4  21901  ovolfiniun  23315  volfiniun  23361  elplyd  24003  ply1term  24005  aannenlem2  24129  aalioulem2  24133  eengbas  25906  ecgrtg  25908  gsumle  29907  reprsuc  30821  bnj1498  31255  mrsubcn  31542  mrsubco  31544  altxpsspw  32209  matunitlindflem1  33535  poimirlem9  33548  poimirlem22  33561  poimirlem31  33570  poimirlem32  33571  mbfresfi  33586  itg2addnclem2  33592  ftc1anclem7  33621  ftc1anc  33623  hdmaplem1  37377  hdmap1eulem  37430  sucidALTVD  39420  sucidALT  39421  founiiun0  39691  mccllem  40147  limcresiooub  40192  limcresioolb  40193  cnrefiisplem  40373  dvmptfprodlem  40477  dvnprodlem2  40480  fourierdlem48  40689  fourierdlem49  40690  fourierdlem51  40692  fourierdlem54  40695  fourierdlem62  40703  fourierdlem71  40712  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  fouriersw  40766  nnfoctbdjlem  40990  hoidmvlelem2  41131  hoidmvlelem3  41132  pimrecltpos  41240  setsnidel  41672
  Copyright terms: Public domain W3C validator