Theorem elun2 4077

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

Syntax hints:   → wi 4   ∈ wcel 2112   ∪ cun 3851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870

This theorem is referenced by:  dftpos4  7965  wfrlem14  8046  tfrlem11  8102  dif1en  8818  findcard2d  8822  cantnfp1lem1  9271  cantnfp1lem3  9273  tc2  9336  rankunb  9431  rankelun  9453  djurcl  9492  djuss  9501  djuun  9507  dfac2b  9709  cfsmolem  9849  isfin4p1  9894  zornn0g  10084  mnfxr  10855  supxrun  12871  fsumsplitsnun  15282  sumsplit  15295  modfsummodslem1  15319  prmreclem5  16436  acsfiindd  18013  lspsolv  20134  mplcoe1  20948  maducoeval2  21491  restntr  22033  1stckgenlem  22404  fbun  22691  filuni  22736  ufileu  22770  alexsubALTlem4  22901  tmdgsum  22946  icccmplem2  23674  aannenlem2  25176  aalioulem2  25180  ebtwntg  27027  elntg  27029  bnj553  32545  bnj966  32591  bnj1442  32696  srcmpltd  32721  mrsubrn  33142  elmrsubrn  33149  mvhf  33187  msubvrs  33189  noetainflem4  33629  addsval  33812  addsid1  33813  addscom  33815  altxpsspw  33965  exrecfnlem  35236  matunitlindflem1  35459  poimirlem3  35466  poimirlem31  35494  poimirlem32  35495  mbfresfi  35509  itg2addnclem2  35515  ftc1anclem7  35542  ftc1anc  35544  hdmaplem2N  39472  hdmaplem3  39473  metakunt22  39809  sucidVD  42106  mccllem  42756  limcresiooub  42801  limcresioolb  42802  cnrefiisplem  42988  dvmptfprodlem  43103  dvmptfprod  43104  dvnprodlem1  43105  dvnprodlem2  43106  fourierdlem20  43286  fourierdlem38  43304  fourierdlem48  43313  fourierdlem49  43314  fourierdlem51  43316  fourierdlem62  43327  fourierdlem63  43328  fourierdlem64  43329  fourierdlem65  43330  fourierdlem71  43336  fouriersw  43390  nnfoctbdjlem  43611  isomenndlem  43686  hoiprodp1  43744  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hspmbllem2  43783  pimrecltpos  43861  setsidel  44444