| 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 7869 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴 ∘ 𝐵) ∈ V) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∘ 𝐵) ∈ V |
| Colors of variables: wff setvar class |
| 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 |
| Copyright terms: Public domain | W3C validator |