![]() |
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 7951 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∘ 𝐵) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3477 ∘ ccom 5692 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 |
This theorem is referenced by: domtr 9045 enfixsn 9119 wdomtr 9612 cfcoflem 10309 axcc3 10475 axdc4uzlem 14020 hashfacen 14489 cofu1st 17933 cofu2nd 17935 cofucl 17938 fucid 18027 sursubmefmnd 18921 injsubmefmnd 18922 smndex1mgm 18932 gsumzaddlem 19953 cnfldfun 21395 cnfldfunALT 21396 cnfldfunOLD 21408 cnfldfunALTOLD 21409 cnfldfunALTOLDOLD 21410 znle 21568 selvval 22156 evls1fval 22338 evls1val 22339 evl1fval 22347 evl1val 22348 xkococnlem 23682 xkococn 23683 efmndtmd 24124 pserulm 26479 imsval 30713 tocycf 33119 eulerpartgbij 34353 derangenlem 35155 subfacp1lem5 35168 poimirlem9 37615 poimirlem15 37621 poimirlem17 37623 poimirlem20 37626 mbfresfi 37652 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 42802 fzisoeu 45250 stirlinglem14 46042 fundcmpsurinjpreimafv 47332 grimco 47817 gricushgr 47823 uspgrlim 47894 grlictr 47910 |
Copyright terms: Public domain | W3C validator |