Theorem coex 7872

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440   ∘ ccom 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635

This theorem is referenced by:  domtr  8944  enfixsn  9014  wdomtr  9480  cfcoflem  10182  axcc3  10348  axdc4uzlem  13906  hashfacen  14377  cofu1st  17807  cofu2nd  17809  cofucl  17812  fucid  17898  sursubmefmnd  18821  injsubmefmnd  18822  smndex1mgm  18832  gsumzaddlem  19850  cnfldfun  21323  cnfldfunALT  21324  cnfldfunOLD  21336  cnfldfunALTOLD  21337  znle  21491  selvval  22078  evls1fval  22263  evls1val  22264  evl1fval  22272  evl1val  22273  xkococnlem  23603  xkococn  23604  efmndtmd  24045  pserulm  26387  imsval  30760  tocycf  33199  eulerpartgbij  34529  derangenlem  35365  subfacp1lem5  35378  poimirlem9  37830  poimirlem15  37836  poimirlem17  37838  poimirlem20  37841  mbfresfi  37867  tendopl2  41037  erngplus2  41064  erngplus2-rN  41072  dvaplusgv  41270  dvhvaddass  41357  dvhlveclem  41368  diblss  41430  diblsmopel  41431  dicvaddcl  41450  dicvscacl  41451  cdlemn7  41463  dihordlem7  41474  dihopelvalcpre  41508  xihopellsmN  41514  dihopellsm  41515  rabren3dioph  43057  fzisoeu  45548  stirlinglem14  46331  fundcmpsurinjpreimafv  47654  grimco  48135  gricushgr  48163  cycldlenngric  48174  uspgrlim  48238  grlictr  48261  fuco22natlem  49590