Theorem fvmptelcdm 7057

Description: The value of a function at a point of its domain belongs to its codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
fvmptelcdm.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Assertion

Ref	Expression
fvmptelcdm	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem fvmptelcdm

Step	Hyp	Ref	Expression
1		fvmptelcdm.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
2		eqid 2737	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	fmpt 7054	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
4	1, 3	sylibr 234	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
5	4	r19.21bi 3230	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3052   ↦ cmpt 5167  ⟶wf 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-fun 6492  df-fn 6493  df-f 6494

This theorem is referenced by:  rlimmptrcl  15532  lo1mptrcl  15546  o1mptrcl  15547  frlmgsum  21729  uvcresum  21750  psrass1lem  21889  txcnp  23563  ptcnp  23565  ptcn  23570  cnmpt11  23606  cnmpt1t  23608  cnmpt12  23610  cnmptkp  23623  cnmptk1  23624  cnmptkk  23626  cnmptk1p  23628  cnmptk2  23629  cnmpt1plusg  24030  cnmpt1vsca  24137  cnmpt1ds  24786  cncfcompt2  24853  cncfmpt2ss  24861  cnmpt1ip  25192  divcncf  25392  mbfmptcl  25581  i1fposd  25652  itgss3  25760  dvmptcl  25904  dvmptco  25917  dvle  25953  dvfsumle  25967  dvfsumleOLD  25968  dvfsumge  25969  dvmptrecl  25971  itgparts  25995  itgsubstlem  25996  itgsubst  25997  ulmss  26346  ulmdvlem2  26350  itgulm2  26358  logtayl  26609  intlewftc  42492  cncfcompt  46315  cncficcgt0  46320  itgsubsticclem  46407  sge0iunmptlemre  46847  hoicvrrex  46988  smfadd  47197  smfpimioompt  47218