![]() |
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 7215 | . 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | |
4 | 1, 2, 3 | syl2anc 585 | 1 ⊢ (𝜑 → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3475 ⟶wf 6531 |
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 5281 ax-sep 5295 ax-nul 5302 ax-pr 5423 |
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 2942 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3776 df-csb 3892 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-iun 4995 df-br 5145 df-opab 5207 df-mpt 5228 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6487 df-fun 6537 df-fn 6538 df-f 6539 df-f1 6540 df-fo 6541 df-f1o 6542 df-fv 6543 |
This theorem is referenced by: fidmfisupp 9359 fdmfisuppfi 9360 fsuppco2 9385 fsuppcor 9386 ixpiunwdom 9572 cnfcom3clem 9687 fin23lem32 10326 hasheqf1od 14300 hashf1lem1 14402 hashf1lem1OLD 14403 fz1isolem 14409 ramval 16928 imasval 17444 imasle 17456 pwsco1mhm 18700 efgtf 19574 gsumval3a 19754 gsumval3lem1 19756 gsumval3lem2 19757 gsumval3 19758 gsumzres 19760 gsumzf1o 19763 gsumzaddlem 19772 gsumzadd 19773 gsumzmhm 19788 gsumzoppg 19795 gsumpt 19813 gsum2dlem2 19822 prdslmodd 20557 dsmmsubg 21271 dsmmlss 21272 islindf2 21342 f1lindf 21350 islindf4 21366 gsumply1subr 21727 txcn 23099 prdstps 23102 qtopval2 23169 fmval 23416 tsmsres 23617 tsmsadd 23620 jensen 26460 pwrssmgc 32141 gsumpart 32178 ply1degltdimlem 32645 ofcfval4 33034 omsfval 33224 omssubadd 33230 carsgval 33233 sseqval 33318 hgt750lemg 33597 filnetlem4 35171 bj-finsumval0 36071 isrngod 36672 isgrpda 36729 iscringd 36772 sticksstones8 40875 limsupre 44230 limsupval3 44281 limsuppnfdlem 44290 limsupvaluz 44297 limsuppnflem 44299 limsupre2lem 44313 climuzlem 44332 climisp 44335 climxrrelem 44338 climxrre 44339 liminfval5 44354 limsupgtlem 44366 liminfvalxr 44372 liminflelimsupuz 44374 liminfgelimsupuz 44377 liminflimsupclim 44396 liminflbuz2 44404 xlimclim2lem 44428 climxlim2 44435 fourierdlem71 44766 fourierdlem80 44775 sge0val 44955 sge0f1o 44971 isomennd 45120 nsssmfmbflem 45367 itcovalendof 47195 |
Copyright terms: Public domain | W3C validator |