ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elun1 GIF version

Theorem elun1 3182
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 3178 . 2 𝐵 ⊆ (𝐵𝐶)
21sseli 3035 1 (𝐴𝐵𝐴 ∈ (𝐵𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1445  cun 3011
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-un 3017  df-in 3019  df-ss 3026
This theorem is referenced by:  dcun  3412  exmidundif  4058  exmidundifim  4059  brtposg  6057  dftpos4  6066  dcdifsnid  6303  undifdcss  6713  fidcenumlemrks  6742  djulclr  6821  djulcl  6823  djuss  6841  finomni  6883  hashennnuni  10318  sumsplitdc  10990  srngbased  11781  srngplusgd  11782  srngmulrd  11783  lmodbased  11792  lmodplusgd  11793  lmodscad  11794  ipsbased  11800  ipsaddgd  11801  ipsmulrd  11802
  Copyright terms: Public domain W3C validator