Theorem coex 7923

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463   ∘ ccom 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pow 5334  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670

This theorem is referenced by:  domtr  9000  enfixsn  9070  wdomtr  9533  cfcoflem  10252  axcc3  10418  axdc4uzlem  14015  hashfacen  14487  cofu1st  17936  cofu2nd  17938  cofucl  17941  fucid  18027  sursubmefmnd  18951  injsubmefmnd  18952  smndex1mgm  18965  gsumzaddlem  19987  cnfldfun  21501  cnfldfunALT  21502  znle  21651  selvval  22236  evls1fval  22444  evls1val  22445  evl1fval  22453  evl1val  22454  xkococnlem  23781  xkococn  23782  efmndtmd  24223  pserulm  26547  imsval  30974  tocycf  33374  eulerpartgbij  34703  derangenlem  35558  subfacp1lem5  35571  poimirlem9  38163  poimirlem15  38169  poimirlem17  38171  poimirlem20  38174  mbfresfi  38200  tendopl2  41436  erngplus2  41463  erngplus2-rN  41471  dvaplusgv  41669  dvhvaddass  41756  dvhlveclem  41767  diblss  41829  diblsmopel  41830  dicvaddcl  41849  dicvscacl  41850  cdlemn7  41862  dihordlem7  41873  dihopelvalcpre  41907  xihopellsmN  41913  dihopellsm  41914  rabren3dioph  43427  fzisoeu  45904  stirlinglem14  46686  fundcmpsurinjpreimafv  48039  grimco  48536  gricushgr  48564  cycldlenngric  48575  uspgrlim  48639  grlictr  48662  fuco22natlem  50001