Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fexd | Structured version Visualization version GIF version |
Description: If the domain of a mapping is a set, the function is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
fexd.1 | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
fexd.2 | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Ref | Expression |
---|---|
fexd | ⊢ (𝜑 → 𝐹 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fexd.1 | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | fexd.2 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶) | |
3 | fex 7111 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3433 ⟶wf 6433 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
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 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4841 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-id 5490 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 |
This theorem is referenced by: fdmfisuppfi 9146 fsuppco2 9171 fsuppcor 9172 ixpiunwdom 9358 cnfcom3clem 9472 fin23lem32 10109 hasheqf1od 14077 hashf1lem1 14177 hashf1lem1OLD 14178 fz1isolem 14184 ramval 16718 imasval 17231 imasle 17243 pwsco1mhm 18479 efgtf 19337 gsumval3a 19513 gsumval3lem1 19515 gsumval3lem2 19516 gsumval3 19517 gsumzres 19519 gsumzf1o 19522 gsumzaddlem 19531 gsumzadd 19532 gsumzmhm 19547 gsumzoppg 19554 gsumpt 19572 gsum2dlem2 19581 prdslmodd 20240 dsmmsubg 20959 dsmmlss 20960 islindf2 21030 f1lindf 21038 islindf4 21054 gsumply1subr 21414 txcn 22786 prdstps 22789 qtopval2 22856 fmval 23103 tsmsres 23304 tsmsadd 23307 jensen 26147 pwrssmgc 31287 gsumpart 31324 ofcfval4 32082 omsfval 32270 omssubadd 32276 carsgval 32279 sseqval 32364 hgt750lemg 32643 filnetlem4 34579 bj-finsumval0 35465 isrngod 36065 isgrpda 36122 iscringd 36165 sticksstones8 40116 fidmfisupp 42746 limsupre 43189 limsupval3 43240 limsuppnfdlem 43249 limsupvaluz 43256 limsuppnflem 43258 limsupre2lem 43272 climuzlem 43291 climisp 43294 climxrrelem 43297 climxrre 43298 liminfval5 43313 limsupgtlem 43325 liminfvalxr 43331 liminflelimsupuz 43333 liminfgelimsupuz 43336 liminflimsupclim 43355 liminflbuz2 43363 xlimclim2lem 43387 climxlim2 43394 fourierdlem71 43725 fourierdlem80 43734 sge0val 43911 sge0f1o 43927 isomennd 44076 nsssmfmbflem 44323 itcovalendof 46026 |
Copyright terms: Public domain | W3C validator |