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 692	1 ⊢ (𝐴 ∘ 𝐵) ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438   ∘ ccom 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634

This theorem is referenced by:  domtr  8939  enfixsn  9010  wdomtr  9486  cfcoflem  10185  axcc3  10351  axdc4uzlem  13908  hashfacen  14379  cofu1st  17808  cofu2nd  17810  cofucl  17813  fucid  17899  sursubmefmnd  18788  injsubmefmnd  18789  smndex1mgm  18799  gsumzaddlem  19818  cnfldfun  21293  cnfldfunALT  21294  cnfldfunOLD  21306  cnfldfunALTOLD  21307  znle  21461  selvval  22038  evls1fval  22222  evls1val  22223  evl1fval  22231  evl1val  22232  xkococnlem  23562  xkococn  23563  efmndtmd  24004  pserulm  26347  imsval  30647  tocycf  33072  eulerpartgbij  34342  derangenlem  35146  subfacp1lem5  35159  poimirlem9  37611  poimirlem15  37617  poimirlem17  37619  poimirlem20  37622  mbfresfi  37648  tendopl2  40759  erngplus2  40786  erngplus2-rN  40794  dvaplusgv  40992  dvhvaddass  41079  dvhlveclem  41090  diblss  41152  diblsmopel  41153  dicvaddcl  41172  dicvscacl  41173  cdlemn7  41185  dihordlem7  41196  dihopelvalcpre  41230  xihopellsmN  41236  dihopellsm  41237  rabren3dioph  42791  fzisoeu  45285  stirlinglem14  46072  fundcmpsurinjpreimafv  47396  grimco  47877  gricushgr  47905  cycldlenngric  47916  uspgrlim  47980  grlictr  48003  fuco22natlem  49334