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 2738 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 2 | fmpt 6984 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
4 | 1, 3 | sylibr 233 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | 4 | r19.21bi 3134 | 1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2106 ∀wral 3064 ↦ cmpt 5157 ⟶wf 6429 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-fun 6435 df-fn 6436 df-f 6437 |
This theorem is referenced by: rlimmptrcl 15317 lo1mptrcl 15331 o1mptrcl 15332 frlmgsum 20979 uvcresum 21000 psrass1lemOLD 21143 psrass1lem 21146 txcnp 22771 ptcnp 22773 ptcn 22778 cnmpt11 22814 cnmpt1t 22816 cnmpt12 22818 cnmptkp 22831 cnmptk1 22832 cnmptkk 22834 cnmptk1p 22836 cnmptk2 22837 cnmpt1plusg 23238 cnmpt1vsca 23345 cnmpt1ds 24005 cncfcompt2 24071 cncfmpt2ss 24079 cnmpt1ip 24411 divcncf 24611 mbfmptcl 24800 i1fposd 24872 itgss3 24979 dvmptcl 25123 dvmptco 25136 dvle 25171 dvfsumle 25185 dvfsumge 25186 dvmptrecl 25188 itgparts 25211 itgsubstlem 25212 itgsubst 25213 ulmss 25556 ulmdvlem2 25560 itgulm2 25568 logtayl 25815 intlewftc 40069 cncfcompt 43424 cncficcgt0 43429 itgsubsticclem 43516 sge0iunmptlemre 43953 hoicvrrex 44094 smfadd 44300 smfpimioompt 44320 smfinfmpt 44352 |
Copyright terms: Public domain | W3C validator |