![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpoex | Structured version Visualization version GIF version |
Description: If the domain of an operation given by maps-to notation is a set, the operation is a set. (Contributed by Mario Carneiro, 20-Dec-2013.) |
Ref | Expression |
---|---|
mpoex.1 | ⊢ 𝐴 ∈ V |
mpoex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
mpoex | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | mpoex.2 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 2 | rgenw 3064 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 ∈ V |
4 | eqid 2731 | . . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) | |
5 | 4 | mpoexxg 8044 | . 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V) |
6 | 1, 3, 5 | mp2an 690 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ∀wral 3060 Vcvv 3473 ∈ cmpo 7395 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-id 5567 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-oprab 7397 df-mpo 7398 df-1st 7957 df-2nd 7958 |
This theorem is referenced by: mptmpoopabbrd 8049 qexALT 12930 ruclem13 16167 vdwapfval 16886 prdsco 17396 imasvsca 17448 homffval 17616 comfffval 17624 comffval 17625 comfffn 17630 comfeq 17632 oppccofval 17643 monfval 17661 sectffval 17679 invffval 17687 cofu1st 17815 cofu2nd 17817 cofucl 17820 natfval 17879 fuccofval 17893 fucco 17897 coafval 17996 setcco 18015 catchomfval 18034 catccofval 18036 catcco 18037 estrcco 18063 xpcval 18111 xpchomfval 18113 xpccofval 18116 xpcco 18117 1stf1 18126 1stf2 18127 2ndf1 18129 2ndf2 18130 1stfcl 18131 2ndfcl 18132 prf1 18134 prf2fval 18135 prfcl 18137 prf1st 18138 prf2nd 18139 evlf2 18153 evlf1 18155 evlfcl 18157 curf1fval 18159 curf11 18161 curf12 18162 curf1cl 18163 curf2 18164 curfcl 18167 hof1fval 18188 hof2fval 18190 hofcl 18194 yonedalem3 18215 efmndplusg 18736 mgmnsgrpex 18787 sgrpnmndex 18788 grpsubfvalALT 18844 mulgfvalALT 18925 symgvalstruct 19228 symgvalstructOLD 19229 lsmfval 19470 pj1fval 19526 dvrfval 20166 psrmulr 21434 psrvscafval 21440 evlslem2 21571 mamufval 21816 mvmulfval 21973 isphtpy 24426 pcofval 24455 q1pval 25600 r1pval 25603 mulsproplem9 27493 motplusg 27658 midf 27892 ismidb 27894 ttgval 27991 ttgvalOLD 27992 ebtwntg 28105 ecgrtg 28106 elntg 28107 wwlksnon 28970 wspthsnon 28971 clwwlknonmpo 29207 vsfval 29749 dipfval 29818 idlsrgmulr 32466 smatfval 32606 lmatval 32624 qqhval 32785 dya2iocuni 33113 sxbrsigalem5 33118 sitmval 33179 signswplusg 33397 reprval 33453 mclsrcl 34383 mclsval 34385 ldualfvs 37811 paddfval 38473 tgrpopr 39423 erngfplus 39478 erngfmul 39481 erngfplus-rN 39486 erngfmul-rN 39489 dvafvadd 39690 dvafvsca 39692 dvaabl 39700 dvhfvadd 39767 dvhfvsca 39776 djafvalN 39810 djhfval 40073 hlhilip 40628 mendplusgfval 41698 mendmulrfval 41700 mendvscafval 41703 mnringmulrd 42751 mnringmulrcld 42758 hoidmvval 45066 cznrng 46501 cznnring 46502 rngchomfvalALTV 46530 rngccofvalALTV 46533 rngccoALTV 46534 ringchomfvalALTV 46593 ringccofvalALTV 46596 ringccoALTV 46597 rrx2xpreen 47053 lines 47065 spheres 47080 functhinclem1 47309 thincciso 47317 |
Copyright terms: Public domain | W3C validator |