Theorem elun1 4205

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  brtpos  8276  dftpos4  8286  domunsncan  9138  unxpdomlem2  9314  rankunb  9919  rankelun  9941  djulcl  9979  djuss  9989  djuun  9995  fin1a2lem10  10478  zornn0g  10574  xrsupexmnf  13367  xrinfmexpnf  13368  sumsplit  15816  lcmfunsnlem2lem1  16685  lcmfunsnlem2  16687  prmreclem5  16967  smndex1mnd  18945  smndex1id  18946  lbsextlem3  21185  restntr  23211  comppfsc  23561  1stckgenlem  23582  fbun  23869  filconn  23912  filuni  23914  alexsubALTlem4  24079  ovolfiniun  25555  volfiniun  25601  elplyd  26261  ply1term  26263  aannenlem2  26389  aalioulem2  26393  cutlt  27984  addsval  28013  addsrid  28015  addscom  28017  addsproplem2  28021  addsproplem6  28025  sleadd1  28040  addsass  28056  negsproplem2  28079  negsproplem6  28083  negsid  28091  mulsval  28153  mulsrid  28157  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsproplem12  28171  mulscom  28183  addsdi  28199  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  eengbas  29014  ecgrtg  29016  gsumle  33074  reprsuc  34592  bnj1498  35037  mrsubcn  35487  mrsubco  35489  altxpsspw  35941  weiunse  36434  matunitlindflem1  37576  poimirlem9  37589  poimirlem22  37602  poimirlem31  37611  poimirlem32  37612  mbfresfi  37626  itg2addnclem2  37632  ftc1anclem7  37659  ftc1anc  37661  hdmaplem1  41728  hdmap1eulem  41779  metakunt21  42182  sucidALTVD  44841  sucidALT  44842  founiiun0  45097  pimxrneun  45404  mccllem  45518  limcresiooub  45563  limcresioolb  45564  cnrefiisplem  45750  dvmptfprodlem  45865  dvnprodlem2  45868  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem62  46089  fourierdlem71  46098  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  fouriersw  46152  nnfoctbdjlem  46376  hoidmvlelem2  46517  hoidmvlelem3  46518  pimrecltpos  46629  setsnidel  47251