Theorem coex 7952

Description: The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.)

Hypotheses

Ref	Expression
coex.1	⊢ 𝐴 ∈ V
coex.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
coex	⊢ (𝐴 ∘ 𝐵) ∈ V

Proof of Theorem coex

Step	Hyp	Ref	Expression
1		coex.1	. 2 ⊢ 𝐴 ∈ V
2		coex.2	. 2 ⊢ 𝐵 ∈ V
3		coexg 7951	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
4	1, 2, 3	mp2an 692	1 ⊢ (𝐴 ∘ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480   ∘ ccom 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696

This theorem is referenced by:  domtr  9047  enfixsn  9121  wdomtr  9615  cfcoflem  10312  axcc3  10478  axdc4uzlem  14024  hashfacen  14493  cofu1st  17928  cofu2nd  17930  cofucl  17933  fucid  18019  sursubmefmnd  18909  injsubmefmnd  18910  smndex1mgm  18920  gsumzaddlem  19939  cnfldfun  21378  cnfldfunALT  21379  cnfldfunOLD  21391  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  znle  21551  selvval  22139  evls1fval  22323  evls1val  22324  evl1fval  22332  evl1val  22333  xkococnlem  23667  xkococn  23668  efmndtmd  24109  pserulm  26465  imsval  30704  tocycf  33137  eulerpartgbij  34374  derangenlem  35176  subfacp1lem5  35189  poimirlem9  37636  poimirlem15  37642  poimirlem17  37644  poimirlem20  37647  mbfresfi  37673  tendopl2  40779  erngplus2  40806  erngplus2-rN  40814  dvaplusgv  41012  dvhvaddass  41099  dvhlveclem  41110  diblss  41172  diblsmopel  41173  dicvaddcl  41192  dicvscacl  41193  cdlemn7  41205  dihordlem7  41216  dihopelvalcpre  41250  xihopellsmN  41256  dihopellsm  41257  rabren3dioph  42826  fzisoeu  45312  stirlinglem14  46102  fundcmpsurinjpreimafv  47395  grimco  47880  gricushgr  47886  uspgrlim  47959  grlictr  47975  fuco22natlem  49040