Theorem elun1 4103

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

Assertion

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

Proof of Theorem elun1

Step	Hyp	Ref	Expression
1		ssun1 4099	. 2 ⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶)
2	1	sseli 3911	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐵 ∪ 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2111   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  brtpos  7884  dftpos4  7894  domunsncan  8600  unxpdomlem2  8707  rankunb  9263  rankelun  9285  djulcl  9323  djuss  9333  djuun  9339  fin1a2lem10  9820  zornn0g  9916  xrsupexmnf  12686  xrinfmexpnf  12687  sumsplit  15115  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  prmreclem5  16246  smndex1mnd  18067  smndex1id  18068  lbsextlem3  19925  restntr  21787  comppfsc  22137  1stckgenlem  22158  fbun  22445  filconn  22488  filuni  22490  alexsubALTlem4  22655  ovolfiniun  24105  volfiniun  24151  elplyd  24799  ply1term  24801  aannenlem2  24925  aalioulem2  24929  eengbas  26775  ecgrtg  26777  gsumle  30775  reprsuc  31996  bnj1498  32443  mrsubcn  32879  mrsubco  32881  altxpsspw  33551  matunitlindflem1  35053  poimirlem9  35066  poimirlem22  35079  poimirlem31  35088  poimirlem32  35089  mbfresfi  35103  itg2addnclem2  35109  ftc1anclem7  35136  ftc1anc  35138  hdmaplem1  39067  hdmap1eulem  39118  metakunt21  39370  sucidALTVD  41576  sucidALT  41577  founiiun0  41817  mccllem  42239  limcresiooub  42284  limcresioolb  42285  cnrefiisplem  42471  dvmptfprodlem  42586  dvnprodlem2  42589  fourierdlem48  42796  fourierdlem49  42797  fourierdlem51  42799  fourierdlem54  42802  fourierdlem62  42810  fourierdlem71  42819  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  fouriersw  42873  nnfoctbdjlem  43094  hoidmvlelem2  43235  hoidmvlelem3  43236  pimrecltpos  43344  setsnidel  43894