Theorem elun2 4135

Description: Membership law for union of classes. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
elun2	⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Proof of Theorem elun2

Step	Hyp	Ref	Expression
1		ssun2 4131	. 2 ⊢ 𝐵 ⊆ (𝐶 ∪ 𝐵)
2	1	sseli 3932	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ (𝐶 ∪ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2142   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is referenced by:  resf1extb  7915  dftpos4  8225  tfrlem11  8359  dif1en  9130  findcard2d  9135  cantnfp1lem1  9633  cantnfp1lem3  9635  tc2  9695  rankunb  9808  rankelun  9830  djurcl  9869  djuss  9878  djuun  9884  dfac2b  10087  cfsmolem  10227  isfin4p1  10272  zornn0g  10462  mnfxr  11239  supxrun  13319  fsumsplitsnun  15782  sumsplit  15795  modfsummodslem1  15820  prmreclem5  16956  acsfiindd  18585  lspsolv  21210  mplcoe1  22087  maducoeval2  22697  restntr  23239  1stckgenlem  23610  fbun  23897  filuni  23942  ufileu  23976  alexsubALTlem4  24107  tmdgsum  24152  icccmplem2  24881  aannenlem2  26390  aalioulem2  26394  noetainflem4  27801  eqcuts3  27894  cutlt  28022  addsval  28052  addsrid  28054  addscom  28056  addsproplem4  28062  addsproplem5  28063  addsproplem6  28064  leadds1  28079  addsass  28095  negsid  28131  mulsval  28199  mulsrid  28203  mulsproplem12  28217  mulscom  28229  addsdi  28245  precsexlem8  28304  precsexlem9  28305  precsexlem11  28307  oncutlt  28354  ebtwntg  29180  elntg  29182  elrspunsn  33612  mplidomlem  33821  bnj553  35190  bnj966  35236  bnj1442  35341  srcmpltd  35372  mrsubrn  35860  elmrsubrn  35867  mvhf  35905  msubvrs  35907  altxpsspw  36324  weiunse  36825  exrecfnlem  37870  matunitlindflem1  38112  poimirlem3  38119  poimirlem31  38147  poimirlem32  38148  mbfresfi  38162  itg2addnclem2  38168  ftc1anclem7  38195  ftc1anc  38197  hdmaplem2N  42393  hdmaplem3  42394  sucidVD  45444  nregmodellem  45589  pimxrneun  46059  mccllem  46170  limcresiooub  46213  limcresioolb  46214  cnrefiisplem  46400  dvmptfprodlem  46515  dvmptfprod  46516  dvnprodlem1  46517  dvnprodlem2  46518  fourierdlem20  46698  fourierdlem38  46716  fourierdlem48  46725  fourierdlem49  46726  fourierdlem51  46728  fourierdlem62  46739  fourierdlem63  46740  fourierdlem64  46741  fourierdlem65  46742  fourierdlem71  46748  fouriersw  46802  nnfoctbdjlem  47026  isomenndlem  47101  hoiprodp1  47159  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem3  47168  hoidmvlelem4  47169  hspmbllem2  47198  pimrecltpos  47279  setsidel  47979