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 7012 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | |
4 | 1, 2, 3 | syl2anc 587 | 1 ⊢ (𝜑 → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 Vcvv 3400 ⟶wf 6346 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-rep 5164 ax-sep 5177 ax-nul 5184 ax-pr 5306 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-reu 3061 df-rab 3063 df-v 3402 df-sbc 3686 df-csb 3801 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4222 df-if 4425 df-sn 4527 df-pr 4529 df-op 4533 df-uni 4807 df-iun 4893 df-br 5041 df-opab 5103 df-mpt 5121 df-id 5439 df-xp 5541 df-rel 5542 df-cnv 5543 df-co 5544 df-dm 5545 df-rn 5546 df-res 5547 df-ima 5548 df-iota 6308 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 |
This theorem is referenced by: fdmfisuppfi 8928 fsuppco2 8953 fsuppcor 8954 ixpiunwdom 9140 cnfcom3clem 9254 fin23lem32 9857 hasheqf1od 13819 hashf1lem1 13919 hashf1lem1OLD 13920 fz1isolem 13926 ramval 16457 imasval 16900 imasle 16912 pwsco1mhm 18125 efgtf 18979 gsumval3a 19155 gsumval3lem1 19157 gsumval3lem2 19158 gsumval3 19159 gsumzres 19161 gsumzf1o 19164 gsumzaddlem 19173 gsumzadd 19174 gsumzmhm 19189 gsumzoppg 19196 gsumpt 19214 gsum2dlem2 19223 prdslmodd 19873 dsmmsubg 20572 dsmmlss 20573 islindf2 20643 f1lindf 20651 islindf4 20667 gsumply1subr 21022 txcn 22390 prdstps 22393 qtopval2 22460 fmval 22707 tsmsres 22908 tsmsadd 22911 jensen 25739 pwrssmgc 30868 gsumpart 30905 ofcfval4 31656 omsfval 31844 omssubadd 31850 carsgval 31853 sseqval 31938 hgt750lemg 32217 filnetlem4 34226 bj-finsumval0 35110 isrngod 35712 isgrpda 35769 iscringd 35812 sticksstones8 39748 fidmfisupp 42318 limsupre 42765 limsupval3 42816 limsuppnfdlem 42825 limsupvaluz 42832 limsuppnflem 42834 limsupre2lem 42848 climuzlem 42867 climisp 42870 climxrrelem 42873 climxrre 42874 liminfval5 42889 limsupgtlem 42901 liminfvalxr 42907 liminflelimsupuz 42909 liminfgelimsupuz 42912 liminflimsupclim 42931 liminflbuz2 42939 xlimclim2lem 42963 climxlim2 42970 fourierdlem71 43301 fourierdlem80 43310 sge0val 43487 sge0f1o 43503 isomennd 43652 nsssmfmbflem 43893 itcovalendof 45597 |
Copyright terms: Public domain | W3C validator |