Theorem elun2 3374

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 3370	. 2 |- B C_ ( C u. B )
2	1	sseli 3222	1 |- ( A e. B -> A e. ( C u. B ) )

Syntax hints:   -> wi 4   e. wcel 2201   u. cun 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-v 2803  df-un 3203  df-in 3205  df-ss 3212

This theorem is referenced by:  dcun  3603  exmidundif  4298  exmidundifim  4299  dftpos4  6434  tfrlemibxssdm  6498  tfrlemi14d  6504  tfr1onlembxssdm  6514  tfr1onlemres  6520  tfrcllembxssdm  6527  tfrcllemres  6533  dcdifsnid  6677  findcard2d  7085  findcard2sd  7086  elssdc  7099  onunsnss  7114  undifdcss  7120  fisseneq  7132  fidcenumlemrks  7157  djurclr  7254  djurcl  7256  djuss  7274  finomni  7344  mnfxr  8241  hashinfuni  11045  fsumsplitsnun  12003  sumsplitdc  12016  modfsummodlem1  12040  exmidunben  13070  bassetsnn  13162  srnginvld  13256  lmodvscad  13274  ipsscad  13286  ipsvscad  13287  ipsipd  13288