Theorem coex 7882

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442   ∘ ccom 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643

This theorem is referenced by:  domtr  8956  enfixsn  9026  wdomtr  9492  cfcoflem  10194  axcc3  10360  axdc4uzlem  13918  hashfacen  14389  cofu1st  17819  cofu2nd  17821  cofucl  17824  fucid  17910  sursubmefmnd  18833  injsubmefmnd  18834  smndex1mgm  18844  gsumzaddlem  19862  cnfldfun  21335  cnfldfunALT  21336  cnfldfunOLD  21348  cnfldfunALTOLD  21349  znle  21503  selvval  22090  evls1fval  22275  evls1val  22276  evl1fval  22284  evl1val  22285  xkococnlem  23615  xkococn  23616  efmndtmd  24057  pserulm  26399  imsval  30772  tocycf  33210  eulerpartgbij  34549  derangenlem  35384  subfacp1lem5  35397  poimirlem9  37877  poimirlem15  37883  poimirlem17  37885  poimirlem20  37888  mbfresfi  37914  tendopl2  41150  erngplus2  41177  erngplus2-rN  41185  dvaplusgv  41383  dvhvaddass  41470  dvhlveclem  41481  diblss  41543  diblsmopel  41544  dicvaddcl  41563  dicvscacl  41564  cdlemn7  41576  dihordlem7  41587  dihopelvalcpre  41621  xihopellsmN  41627  dihopellsm  41628  rabren3dioph  43169  fzisoeu  45659  stirlinglem14  46442  fundcmpsurinjpreimafv  47765  grimco  48246  gricushgr  48274  cycldlenngric  48285  uspgrlim  48349  grlictr  48372  fuco22natlem  49701