Theorem elun1 4135

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∪ cun 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  resf1extb  7937  brtpos  8237  dftpos4  8247  domunsncan  9072  unxpdomlem2  9224  rankunb  9829  rankelun  9851  djulcl  9912  djuss  9922  djuun  9928  fin1a2lem10  10408  zornn0g  10504  xrsupexmnf  13349  xrinfmexpnf  13350  sumsplit  15844  lcmfunsnlem2lem1  16720  lcmfunsnlem2  16722  prmreclem5  17004  smndex1mnd  19011  smndex1id  19012  gsumle  20261  lbsextlem3  21336  restntr  23391  comppfsc  23742  1stckgenlem  23763  fbun  24050  filconn  24093  filuni  24095  alexsubALTlem4  24260  ovolfiniun  25713  volfiniun  25759  elplyd  26412  ply1term  26414  aannenlem2  26545  aalioulem2  26549  eqcuts3  28050  cutlt  28178  addsval  28208  addsrid  28210  addscom  28212  addsproplem2  28216  addsproplem6  28220  leadds1  28235  addsass  28251  negsproplem2  28275  negsproplem6  28279  negsid  28287  mulsval  28355  mulsrid  28359  mulsproplem2  28363  mulsproplem3  28364  mulsproplem4  28365  mulsproplem5  28366  mulsproplem6  28367  mulsproplem7  28368  mulsproplem8  28369  mulsproplem12  28373  mulscom  28385  addsdi  28401  precsexlem8  28460  precsexlem9  28461  precsexlem11  28463  eengbas  29388  ecgrtg  29390  reprsuc  35069  bnj1498  35516  mrsubcn  36050  mrsubco  36052  altxpsspw  36508  weiunse  37038  matunitlindflem1  38326  poimirlem9  38339  poimirlem22  38352  poimirlem31  38361  poimirlem32  38362  mbfresfi  38376  itg2addnclem2  38382  ftc1anclem7  38409  ftc1anc  38411  hdmaplem1  42605  hdmap1eulem  42656  sucidALTVD  45638  sucidALT  45639  founiiun0  45968  pimxrneun  46262  mccllem  46373  limcresiooub  46416  limcresioolb  46417  cnrefiisplem  46603  dvmptfprodlem  46718  dvnprodlem2  46721  fourierdlem48  46928  fourierdlem49  46929  fourierdlem51  46931  fourierdlem54  46934  fourierdlem62  46942  fourierdlem71  46951  fourierdlem103  46983  fourierdlem104  46984  fourierdlem114  46994  fouriersw  47005  nnfoctbdjlem  47229  hoidmvlelem2  47370  hoidmvlelem3  47371  pimrecltpos  47482  setsnidel  48186