Theorem elun1 4066

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∪ cun 3841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-in 3850  df-ss 3860

This theorem is referenced by:  brtpos  7932  dftpos4  7942  domunsncan  8668  unxpdomlem2  8804  rankunb  9354  rankelun  9376  djulcl  9414  djuss  9424  djuun  9430  fin1a2lem10  9911  zornn0g  10007  xrsupexmnf  12783  xrinfmexpnf  12784  sumsplit  15218  lcmfunsnlem2lem1  16081  lcmfunsnlem2  16083  prmreclem5  16358  smndex1mnd  18193  smndex1id  18194  lbsextlem3  20053  restntr  21935  comppfsc  22285  1stckgenlem  22306  fbun  22593  filconn  22636  filuni  22638  alexsubALTlem4  22803  ovolfiniun  24255  volfiniun  24301  elplyd  24953  ply1term  24955  aannenlem2  25079  aalioulem2  25083  eengbas  26929  ecgrtg  26931  gsumle  30929  reprsuc  32167  bnj1498  32614  mrsubcn  33054  mrsubco  33056  addsval  33771  addsid1  33772  addscom  33774  altxpsspw  33924  matunitlindflem1  35418  poimirlem9  35431  poimirlem22  35444  poimirlem31  35453  poimirlem32  35454  mbfresfi  35468  itg2addnclem2  35474  ftc1anclem7  35501  ftc1anc  35503  hdmaplem1  39430  hdmap1eulem  39481  metakunt21  39758  sucidALTVD  42050  sucidALT  42051  founiiun0  42288  mccllem  42702  limcresiooub  42747  limcresioolb  42748  cnrefiisplem  42934  dvmptfprodlem  43049  dvnprodlem2  43052  fourierdlem48  43259  fourierdlem49  43260  fourierdlem51  43262  fourierdlem54  43265  fourierdlem62  43273  fourierdlem71  43282  fourierdlem103  43314  fourierdlem104  43315  fourierdlem114  43325  fouriersw  43336  nnfoctbdjlem  43557  hoidmvlelem2  43698  hoidmvlelem3  43699  pimrecltpos  43807  setsnidel  44392