Theorem elun2 3301

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

Assertion

Ref	Expression
elun2	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Proof of Theorem elun2

Step	Hyp	Ref	Expression
1		ssun2 3297	. 2 ⊢ 𝐵 ⊆ (𝐶 ∪ 𝐵)
2	1	sseli 3149	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2146   ∪ cun 3125

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-in 3133  df-ss 3140

This theorem is referenced by:  dcun  3531  exmidundif  4201  exmidundifim  4202  dftpos4  6254  tfrlemibxssdm  6318  tfrlemi14d  6324  tfr1onlembxssdm  6334  tfr1onlemres  6340  tfrcllembxssdm  6347  tfrcllemres  6353  dcdifsnid  6495  findcard2d  6881  findcard2sd  6882  onunsnss  6906  undifdcss  6912  fisseneq  6921  fidcenumlemrks  6942  djurclr  7039  djurcl  7041  djuss  7059  finomni  7128  mnfxr  7988  hashinfuni  10723  fsumsplitsnun  11393  sumsplitdc  11406  modfsummodlem1  11430  exmidunben  12392  srnginvld  12555  lmodvscad  12569  ipsscad  12577  ipsvscad  12578  ipsipd  12579