Theorem elun2 3295

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 3291	. 2 ⊢ 𝐵 ⊆ (𝐶 ∪ 𝐵)
2	1	sseli 3143	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2141   ∪ cun 3119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-in 3127  df-ss 3134

This theorem is referenced by:  dcun  3525  exmidundif  4192  exmidundifim  4193  dftpos4  6242  tfrlemibxssdm  6306  tfrlemi14d  6312  tfr1onlembxssdm  6322  tfr1onlemres  6328  tfrcllembxssdm  6335  tfrcllemres  6341  dcdifsnid  6483  findcard2d  6869  findcard2sd  6870  onunsnss  6894  undifdcss  6900  fisseneq  6909  fidcenumlemrks  6930  djurclr  7027  djurcl  7029  djuss  7047  finomni  7116  mnfxr  7976  hashinfuni  10711  fsumsplitsnun  11382  sumsplitdc  11395  modfsummodlem1  11419  exmidunben  12381  srnginvld  12544  lmodvscad  12555  ipsscad  12563  ipsvscad  12564  ipsipd  12565