Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fvmptelrn | Structured version Visualization version GIF version |
Description: The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
fvmptelrn.1 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
Ref | Expression |
---|---|
fvmptelrn | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmptelrn.1 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) | |
2 | eqid 2821 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 2 | fmpt 6874 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
4 | 1, 3 | sylibr 236 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | 4 | r19.21bi 3208 | 1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 ∀wral 3138 ↦ cmpt 5146 ⟶wf 6351 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pr 5330 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-mpt 5147 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-fv 6363 |
This theorem is referenced by: rlimmptrcl 14964 lo1mptrcl 14978 o1mptrcl 14979 psrass1lem 20157 frlmgsum 20916 uvcresum 20937 txcnp 22228 ptcnp 22230 ptcn 22235 cnmpt11 22271 cnmpt1t 22273 cnmpt12 22275 cnmptkp 22288 cnmptk1 22289 cnmptkk 22291 cnmptk1p 22293 cnmptk2 22294 cnmpt1plusg 22695 cnmpt1vsca 22802 cnmpt1ds 23450 cncfmpt2ss 23523 cnmpt1ip 23850 divcncf 24048 mbfmptcl 24237 i1fposd 24308 itgss3 24415 dvmptcl 24556 dvmptco 24569 dvle 24604 dvfsumle 24618 dvfsumge 24619 dvmptrecl 24621 itgparts 24644 itgsubstlem 24645 itgsubst 24646 ulmss 24985 ulmdvlem2 24989 itgulm2 24997 logtayl 25243 cncfcompt 42186 cncficcgt0 42191 cncfcompt2 42202 itgsubsticclem 42280 sge0iunmptlemre 42717 hoicvrrex 42858 smfadd 43061 smfpimioompt 43081 smfsupmpt 43109 smfinfmpt 43113 |
Copyright terms: Public domain | W3C validator |