Theorem coex 7928

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455   ∘ ccom 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674

This theorem is referenced by:  domtr  9005  enfixsn  9075  wdomtr  9538  cfcoflem  10257  axcc3  10423  axdc4uzlem  14021  hashfacen  14493  cofu1st  17941  cofu2nd  17943  cofucl  17946  fucid  18032  sursubmefmnd  18956  injsubmefmnd  18957  smndex1mgm  18970  gsumzaddlem  19992  cnfldfun  21517  cnfldfunALT  21518  znle  21667  selvval  22252  evls1fval  22460  evls1val  22461  evl1fval  22469  evl1val  22470  xkococnlem  23797  xkococn  23798  efmndtmd  24239  pserulm  26566  imsval  31018  tocycf  33418  eulerpartgbij  34743  derangenlem  35644  subfacp1lem5  35657  poimirlem9  38261  poimirlem15  38267  poimirlem17  38269  poimirlem20  38272  mbfresfi  38298  tendopl2  41532  erngplus2  41559  erngplus2-rN  41567  dvaplusgv  41765  dvhvaddass  41852  dvhlveclem  41863  diblss  41925  diblsmopel  41926  dicvaddcl  41945  dicvscacl  41946  cdlemn7  41958  dihordlem7  41969  dihopelvalcpre  42003  xihopellsmN  42009  dihopellsm  42010  rabren3dioph  43525  fzisoeu  46002  stirlinglem14  46784  fundcmpsurinjpreimafv  48140  grimco  48637  gricushgr  48665  cycldlenngric  48676  uspgrlim  48740  grlictr  48763  fuco22natlem  50106