Theorem coex 7870

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431   ∘ ccom 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629

This theorem is referenced by:  domtr  8944  enfixsn  9014  wdomtr  9480  cfcoflem  10185  axcc3  10351  axdc4uzlem  13936  hashfacen  14407  cofu1st  17841  cofu2nd  17843  cofucl  17846  fucid  17932  sursubmefmnd  18855  injsubmefmnd  18856  smndex1mgm  18869  gsumzaddlem  19887  cnfldfun  21361  cnfldfunALT  21362  znle  21511  selvval  22096  evls1fval  22305  evls1val  22306  evl1fval  22314  evl1val  22315  xkococnlem  23642  xkococn  23643  efmndtmd  24084  pserulm  26405  imsval  30774  tocycf  33198  eulerpartgbij  34556  derangenlem  35399  subfacp1lem5  35412  poimirlem9  37996  poimirlem15  38002  poimirlem17  38004  poimirlem20  38007  mbfresfi  38033  tendopl2  41269  erngplus2  41296  erngplus2-rN  41304  dvaplusgv  41502  dvhvaddass  41589  dvhlveclem  41600  diblss  41662  diblsmopel  41663  dicvaddcl  41682  dicvscacl  41683  cdlemn7  41695  dihordlem7  41706  dihopelvalcpre  41740  xihopellsmN  41746  dihopellsm  41747  rabren3dioph  43260  fzisoeu  45748  stirlinglem14  46530  fundcmpsurinjpreimafv  47883  grimco  48380  gricushgr  48408  cycldlenngric  48419  uspgrlim  48483  grlictr  48506  fuco22natlem  49835