Theorem coex 7915

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 7914	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V)
4	1, 2, 3	mp2an 691	1 ⊢ (𝐴 ∘ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3475   ∘ ccom 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-br 5147  df-opab 5209  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685

This theorem is referenced by:  domtr  8998  enfixsn  9076  wdomtr  9565  cfcoflem  10262  axcc3  10428  axdc4uzlem  13943  hashfacen  14408  hashfacenOLD  14409  cofu1st  17828  cofu2nd  17830  cofucl  17833  fucid  17919  sursubmefmnd  18772  injsubmefmnd  18773  smndex1mgm  18783  gsumzaddlem  19780  cnfldfun  20940  cnfldfunALT  20941  cnfldfunALTOLD  20942  znle  21071  selvval  21662  evls1fval  21819  evls1val  21820  evl1fval  21828  evl1val  21829  xkococnlem  23144  xkococn  23145  efmndtmd  23586  pserulm  25915  imsval  29915  tocycf  32253  eulerpartgbij  33308  derangenlem  34099  subfacp1lem5  34112  poimirlem9  36434  poimirlem15  36440  poimirlem17  36442  poimirlem20  36445  mbfresfi  36471  tendopl2  39585  erngplus2  39612  erngplus2-rN  39620  dvaplusgv  39818  dvhvaddass  39905  dvhlveclem  39916  diblss  39978  diblsmopel  39979  dicvaddcl  39998  dicvscacl  39999  cdlemn7  40011  dihordlem7  40022  dihopelvalcpre  40056  xihopellsmN  40062  dihopellsm  40063  rabren3dioph  41485  fzisoeu  43944  stirlinglem14  44737  fundcmpsurinjpreimafv  46010  isomushgr  46428  isomgrtr  46441