![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > coex | Structured version Visualization version GIF version |
Description: The composition of two sets is a set. (Contributed by NM, 15-Dec-2003.) |
Ref | Expression |
---|---|
coex.1 | ⊢ 𝐴 ∈ V |
coex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
coex | ⊢ (𝐴 ∘ 𝐵) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | coex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | coex.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | coexg 7616 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ (𝐴 ∘ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2111 Vcvv 3441 ∘ ccom 5523 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 |
This theorem is referenced by: domtr 8545 enfixsn 8609 wdomtr 9023 cfcoflem 9683 axcc3 9849 axdc4uzlem 13346 hashfacen 13808 cofu1st 17145 cofu2nd 17147 cofucl 17150 fucid 17233 sursubmefmnd 18053 injsubmefmnd 18054 smndex1mgm 18064 gsumzaddlem 19034 cnfldfun 20103 cnfldfunALT 20104 znle 20228 selvval 20790 evls1fval 20943 evls1val 20944 evl1fval 20952 evl1val 20953 xkococnlem 22264 xkococn 22265 efmndtmd 22706 pserulm 25017 imsval 28468 tocycf 30809 eulerpartgbij 31740 derangenlem 32531 subfacp1lem5 32544 poimirlem9 35066 poimirlem15 35072 poimirlem17 35074 poimirlem20 35077 mbfresfi 35103 tendopl2 38073 erngplus2 38100 erngplus2-rN 38108 dvaplusgv 38306 dvhvaddass 38393 dvhlveclem 38404 diblss 38466 diblsmopel 38467 dicvaddcl 38486 dicvscacl 38487 cdlemn7 38499 dihordlem7 38510 dihopelvalcpre 38544 xihopellsmN 38550 dihopellsm 38551 rabren3dioph 39756 fzisoeu 41932 stirlinglem14 42729 fundcmpsurinjpreimafv 43925 isomushgr 44344 isomgrtr 44357 |
Copyright terms: Public domain | W3C validator |