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 6878 | . . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶) |
4 | 1, 3 | sylibr 237 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶) |
5 | 4 | r19.21bi 3120 | 1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2113 ∀wral 3053 ↦ cmpt 5107 ⟶wf 6329 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-fun 6335 df-fn 6336 df-f 6337 |
This theorem is referenced by: rlimmptrcl 15048 lo1mptrcl 15062 o1mptrcl 15063 frlmgsum 20581 uvcresum 20602 psrass1lemOLD 20746 psrass1lem 20749 txcnp 22364 ptcnp 22366 ptcn 22371 cnmpt11 22407 cnmpt1t 22409 cnmpt12 22411 cnmptkp 22424 cnmptk1 22425 cnmptkk 22427 cnmptk1p 22429 cnmptk2 22430 cnmpt1plusg 22831 cnmpt1vsca 22938 cnmpt1ds 23587 cncfcompt2 23653 cncfmpt2ss 23661 cnmpt1ip 23992 divcncf 24192 mbfmptcl 24381 i1fposd 24452 itgss3 24559 dvmptcl 24703 dvmptco 24716 dvle 24751 dvfsumle 24765 dvfsumge 24766 dvmptrecl 24768 itgparts 24791 itgsubstlem 24792 itgsubst 24793 ulmss 25136 ulmdvlem2 25140 itgulm2 25148 logtayl 25395 intlewftc 39678 cncfcompt 42950 cncficcgt0 42955 itgsubsticclem 43042 sge0iunmptlemre 43479 hoicvrrex 43620 smfadd 43823 smfpimioompt 43843 smfsupmpt 43871 smfinfmpt 43875 |
Copyright terms: Public domain | W3C validator |