Theorem coex 7777

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432   ∘ ccom 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600

This theorem is referenced by:  domtr  8793  enfixsn  8868  wdomtr  9334  cfcoflem  10028  axcc3  10194  axdc4uzlem  13703  hashfacen  14166  hashfacenOLD  14167  cofu1st  17598  cofu2nd  17600  cofucl  17603  fucid  17689  sursubmefmnd  18535  injsubmefmnd  18536  smndex1mgm  18546  gsumzaddlem  19522  cnfldfun  20609  cnfldfunALT  20610  cnfldfunALTOLD  20611  znle  20740  selvval  21328  evls1fval  21485  evls1val  21486  evl1fval  21494  evl1val  21495  xkococnlem  22810  xkococn  22811  efmndtmd  23252  pserulm  25581  imsval  29047  tocycf  31384  eulerpartgbij  32339  derangenlem  33133  subfacp1lem5  33146  poimirlem9  35786  poimirlem15  35792  poimirlem17  35794  poimirlem20  35797  mbfresfi  35823  tendopl2  38791  erngplus2  38818  erngplus2-rN  38826  dvaplusgv  39024  dvhvaddass  39111  dvhlveclem  39122  diblss  39184  diblsmopel  39185  dicvaddcl  39204  dicvscacl  39205  cdlemn7  39217  dihordlem7  39228  dihopelvalcpre  39262  xihopellsmN  39268  dihopellsm  39269  rabren3dioph  40637  fzisoeu  42839  stirlinglem14  43628  fundcmpsurinjpreimafv  44860  isomushgr  45278  isomgrtr  45291