Theorem elun1 4151

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

Syntax hints:   → wi 4   ∈ wcel 2110   ∪ cun 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3940  df-in 3942  df-ss 3951

This theorem is referenced by:  brtpos  7895  dftpos4  7905  domunsncan  8611  unxpdomlem2  8717  rankunb  9273  rankelun  9295  djulcl  9333  djuss  9343  djuun  9349  fin1a2lem10  9825  zornn0g  9921  xrsupexmnf  12692  xrinfmexpnf  12693  sumsplit  15117  lcmfunsnlem2lem1  15976  lcmfunsnlem2  15978  prmreclem5  16250  smndex1mnd  18069  smndex1id  18070  lbsextlem3  19926  restntr  21784  comppfsc  22134  1stckgenlem  22155  fbun  22442  filconn  22485  filuni  22487  alexsubALTlem4  22652  ovolfiniun  24096  volfiniun  24142  elplyd  24786  ply1term  24788  aannenlem2  24912  aalioulem2  24916  eengbas  26761  ecgrtg  26763  gsumle  30720  reprsuc  31881  bnj1498  32328  mrsubcn  32761  mrsubco  32763  altxpsspw  33433  matunitlindflem1  34882  poimirlem9  34895  poimirlem22  34908  poimirlem31  34917  poimirlem32  34918  mbfresfi  34932  itg2addnclem2  34938  ftc1anclem7  34967  ftc1anc  34969  hdmaplem1  38901  hdmap1eulem  38952  sucidALTVD  41197  sucidALT  41198  founiiun0  41444  mccllem  41871  limcresiooub  41916  limcresioolb  41917  cnrefiisplem  42103  dvmptfprodlem  42222  dvnprodlem2  42225  fourierdlem48  42433  fourierdlem49  42434  fourierdlem51  42436  fourierdlem54  42439  fourierdlem62  42447  fourierdlem71  42456  fourierdlem103  42488  fourierdlem104  42489  fourierdlem114  42499  fouriersw  42510  nnfoctbdjlem  42731  hoidmvlelem2  42872  hoidmvlelem3  42873  pimrecltpos  42981  setsnidel  43531