![]() |
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 7177 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | |
4 | 1, 2, 3 | syl2anc 585 | 1 ⊢ (𝜑 → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3444 ⟶wf 6493 |
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 2704 ax-rep 5243 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 |
This theorem is referenced by: fidmfisupp 9318 fdmfisuppfi 9319 fsuppco2 9344 fsuppcor 9345 ixpiunwdom 9531 cnfcom3clem 9646 fin23lem32 10285 hasheqf1od 14259 hashf1lem1 14359 hashf1lem1OLD 14360 fz1isolem 14366 ramval 16885 imasval 17398 imasle 17410 pwsco1mhm 18647 efgtf 19509 gsumval3a 19685 gsumval3lem1 19687 gsumval3lem2 19688 gsumval3 19689 gsumzres 19691 gsumzf1o 19694 gsumzaddlem 19703 gsumzadd 19704 gsumzmhm 19719 gsumzoppg 19726 gsumpt 19744 gsum2dlem2 19753 prdslmodd 20445 dsmmsubg 21165 dsmmlss 21166 islindf2 21236 f1lindf 21244 islindf4 21260 gsumply1subr 21621 txcn 22993 prdstps 22996 qtopval2 23063 fmval 23310 tsmsres 23511 tsmsadd 23514 jensen 26354 pwrssmgc 31909 gsumpart 31946 ply1degltdimlem 32374 ofcfval4 32761 omsfval 32951 omssubadd 32957 carsgval 32960 sseqval 33045 hgt750lemg 33324 filnetlem4 34899 bj-finsumval0 35802 isrngod 36403 isgrpda 36460 iscringd 36503 sticksstones8 40607 limsupre 43968 limsupval3 44019 limsuppnfdlem 44028 limsupvaluz 44035 limsuppnflem 44037 limsupre2lem 44051 climuzlem 44070 climisp 44073 climxrrelem 44076 climxrre 44077 liminfval5 44092 limsupgtlem 44104 liminfvalxr 44110 liminflelimsupuz 44112 liminfgelimsupuz 44115 liminflimsupclim 44134 liminflbuz2 44142 xlimclim2lem 44166 climxlim2 44173 fourierdlem71 44504 fourierdlem80 44513 sge0val 44693 sge0f1o 44709 isomennd 44858 nsssmfmbflem 45105 itcovalendof 46841 |
Copyright terms: Public domain | W3C validator |