Theorem elun1 4110

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  brtpos  8051  dftpos4  8061  domunsncan  8859  unxpdomlem2  9028  rankunb  9608  rankelun  9630  djulcl  9668  djuss  9678  djuun  9684  fin1a2lem10  10165  zornn0g  10261  xrsupexmnf  13039  xrinfmexpnf  13040  sumsplit  15480  lcmfunsnlem2lem1  16343  lcmfunsnlem2  16345  prmreclem5  16621  smndex1mnd  18549  smndex1id  18550  lbsextlem3  20422  restntr  22333  comppfsc  22683  1stckgenlem  22704  fbun  22991  filconn  23034  filuni  23036  alexsubALTlem4  23201  ovolfiniun  24665  volfiniun  24711  elplyd  25363  ply1term  25365  aannenlem2  25489  aalioulem2  25493  eengbas  27349  ecgrtg  27351  gsumle  31350  reprsuc  32595  bnj1498  33041  mrsubcn  33481  mrsubco  33483  addsval  34126  addsid1  34127  addscom  34129  altxpsspw  34279  matunitlindflem1  35773  poimirlem9  35786  poimirlem22  35799  poimirlem31  35808  poimirlem32  35809  mbfresfi  35823  itg2addnclem2  35829  ftc1anclem7  35856  ftc1anc  35858  hdmaplem1  39785  hdmap1eulem  39836  metakunt21  40145  sucidALTVD  42490  sucidALT  42491  founiiun0  42728  mccllem  43138  limcresiooub  43183  limcresioolb  43184  cnrefiisplem  43370  dvmptfprodlem  43485  dvnprodlem2  43488  fourierdlem48  43695  fourierdlem49  43696  fourierdlem51  43698  fourierdlem54  43701  fourierdlem62  43709  fourierdlem71  43718  fourierdlem103  43750  fourierdlem104  43751  fourierdlem114  43761  fouriersw  43772  nnfoctbdjlem  43993  hoidmvlelem2  44134  hoidmvlelem3  44135  pimrecltpos  44245  setsnidel  44829