Theorem coex 7909

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450   ∘ ccom 5645

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-10 2142  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652

This theorem is referenced by:  domtr  8981  enfixsn  9055  wdomtr  9535  cfcoflem  10232  axcc3  10398  axdc4uzlem  13955  hashfacen  14426  cofu1st  17852  cofu2nd  17854  cofucl  17857  fucid  17943  sursubmefmnd  18830  injsubmefmnd  18831  smndex1mgm  18841  gsumzaddlem  19858  cnfldfun  21285  cnfldfunALT  21286  cnfldfunOLD  21298  cnfldfunALTOLD  21299  znle  21453  selvval  22029  evls1fval  22213  evls1val  22214  evl1fval  22222  evl1val  22223  xkococnlem  23553  xkococn  23554  efmndtmd  23995  pserulm  26338  imsval  30621  tocycf  33081  eulerpartgbij  34370  derangenlem  35165  subfacp1lem5  35178  poimirlem9  37630  poimirlem15  37636  poimirlem17  37638  poimirlem20  37641  mbfresfi  37667  tendopl2  40778  erngplus2  40805  erngplus2-rN  40813  dvaplusgv  41011  dvhvaddass  41098  dvhlveclem  41109  diblss  41171  diblsmopel  41172  dicvaddcl  41191  dicvscacl  41192  cdlemn7  41204  dihordlem7  41215  dihopelvalcpre  41249  xihopellsmN  41255  dihopellsm  41256  rabren3dioph  42810  fzisoeu  45305  stirlinglem14  46092  fundcmpsurinjpreimafv  47413  grimco  47893  gricushgr  47921  cycldlenngric  47932  uspgrlim  47995  grlictr  48011  fuco22natlem  49338