Theorem coex 7976

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454   ∘ ccom 5662

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669

This theorem is used by:  domtr  9072  enfixsn  9143  wdomtr  9606  cfcoflem  10389  axcc3  10555  axdc4uzlem  14166  hashfacen  14640  cofu1st  18108  cofu2nd  18110  cofucl  18113  fucid  18199  sursubmefmnd  19142  injsubmefmnd  19143  smndex1mgm  19156  gsumzaddlem  20186  cnfldfun  21744  cnfldfunALT  21745  znle  21897  selvval  22484  evls1fval  22692  evls1val  22693  evl1fval  22701  evl1val  22702  xkococnlem  24033  xkococn  24034  efmndtmd  24475  pserulm  26806  imsval  31344  tocycf  33777  eulerpartgbij  35115  derangenlem  36144  subfacp1lem5  36157  poimirlem9  38815  poimirlem15  38821  poimirlem17  38823  poimirlem20  38826  mbfresfi  38852  tendopl2  42100  erngplus2  42127  erngplus2-rN  42135  dvaplusgv  42333  dvhvaddass  42420  dvhlveclem  42431  diblss  42493  diblsmopel  42494  dicvaddcl  42513  dicvscacl  42514  cdlemn7  42526  dihordlem7  42537  dihopelvalcpre  42571  xihopellsmN  42577  dihopellsm  42578  rabren3dioph  44088  fzisoeu  46589  stirlinglem14  47370  fundcmpsurinjpreimafv  48763  grimco  49260  gricushgr  49288  cycldlenngric  49299  uspgrlim  49363  grlictr  49386  fuco22natlem  50798