Theorem elun2 3208

Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
elun2	|- ( A e. B -> A e. ( C u. B ) )

Proof of Theorem elun2

Step	Hyp	Ref	Expression
1		ssun2 3204	. 2 |- B C_ ( C u. B )
2	1	sseli 3057	1 |- ( A e. B -> A e. ( C u. B ) )

Syntax hints:   -> wi 4   e. wcel 1461   u. cun 3033

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 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-un 3039  df-in 3041  df-ss 3048

This theorem is referenced by:  dcun  3437  exmidundif  4087  exmidundifim  4088  dftpos4  6111  tfrlemibxssdm  6175  tfrlemi14d  6181  tfr1onlembxssdm  6191  tfr1onlemres  6197  tfrcllembxssdm  6204  tfrcllemres  6210  dcdifsnid  6351  findcard2d  6735  findcard2sd  6736  onunsnss  6755  undifdcss  6761  fisseneq  6770  fidcenumlemrks  6790  djurclr  6884  djurcl  6886  djuss  6904  finomni  6959  mnfxr  7739  hashinfuni  10409  fsumsplitsnun  11073  sumsplitdc  11086  modfsummodlem1  11110  exmidunben  11777  srnginvld  11921  lmodvscad  11932  ipsscad  11940  ipsvscad  11941  ipsipd  11942