Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fex | Structured version Visualization version GIF version |
Description: If the domain of a mapping is a set, the function is a set. (Contributed by NM, 3-Oct-1999.) |
Ref | Expression |
---|---|
fex | ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5958 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fnex 6386 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) | |
3 | 1, 2 | sylan 487 | 1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝐶) → 𝐹 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∈ wcel 1977 Vcvv 3173 Fn wfn 5799 ⟶wf 5800 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pr 4833 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 |
This theorem is referenced by: f1oexrnex 7008 frnsuppeq 7194 suppsnop 7196 f1domg 7861 fdmfisuppfi 8167 frnfsuppbi 8187 fsuppco2 8191 fsuppcor 8192 mapfienlem2 8194 ordtypelem10 8315 oiexg 8323 cnfcom3clem 8485 infxpenc2lem2 8726 fin23lem32 9049 isf32lem10 9067 focdmex 13001 hasheqf1oi 13002 hashf1rn 13004 hashf1rnOLD 13005 hasheqf1od 13006 hashimarn 13085 hashf1lem1 13096 fz1isolem 13102 iswrd 13162 climsup 14248 fsum 14298 supcvg 14427 fprod 14510 vdwmc 15520 vdwpc 15522 ramval 15550 imasval 15994 imasle 16006 pwsco1mhm 17193 isghm 17483 elsymgbas 17625 gsumval3a 18127 gsumval3lem1 18129 gsumval3lem2 18130 gsumzres 18133 gsumzf1o 18136 gsumzaddlem 18144 gsumzadd 18145 gsumzmhm 18160 gsumzoppg 18167 gsumpt 18184 gsum2dlem2 18193 dmdprd 18220 prdslmodd 18790 gsumply1subr 19425 dsmmsubg 19906 dsmmlss 19907 islindf2 19972 f1lindf 19980 islindf4 19996 prdstps 21242 qtopval2 21309 tsmsres 21757 tngngp3 22270 climcncf 22511 itg2gt0 23333 ulmval 23938 pserulm 23980 jensen 24515 isismt 25229 iseupa 26492 isgrpoi 26736 isvcOLD 26818 isnv 26851 cnnvg 26917 cnnvs 26919 cnnvnm 26920 cncph 27058 ajval 27101 hvmulex 27252 hhph 27419 hlimi 27429 chlimi 27475 hhssva 27498 hhsssm 27499 hhssnm 27500 hhshsslem1 27508 elunop 28115 adjeq 28178 leoprf2 28370 fpwrelmapffslem 28895 lmdvg 29327 esumpfinvallem 29463 ofcfval4 29494 omsfval 29683 omsf 29685 omssubadd 29689 carsgval 29692 eulerpartgbij 29761 eulerpartlemmf 29764 sseqval 29777 subfacp1lem5 30420 sinccvglem 30820 elno 31043 filnetlem4 31546 bj-finsumval0 32324 poimirlem24 32603 mbfresfi 32626 elghomlem2OLD 32855 isrngod 32867 isgrpda 32924 iscringd 32967 islaut 34387 ispautN 34403 istendo 35066 binomcxplemnotnn0 37577 fexd 38327 fidmfisupp 38385 climexp 38672 climinf 38673 limsupre 38708 stirlinglem8 38974 fourierdlem70 39069 fourierdlem71 39070 fourierdlem80 39079 sge0val 39259 sge0f1o 39275 ismea 39344 meadjiunlem 39358 isomennd 39421 usgr2pth 40970 isassintop 41636 fdivmpt 42132 elbigolo1 42149 |
Copyright terms: Public domain | W3C validator |