Theorem fvmptelcdm 7111

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 2761	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	fmpt 7108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
4	1, 3	sylibr 237	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
5	4	r19.21bi 3255	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077   ↦ cmpt 5186  ⟶wf 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  rlimmptrcl  15768  lo1mptrcl  15782  o1mptrcl  15783  frlmgsum  22071  uvcresum  22092  psrass1lem  22234  txcnp  23932  ptcnp  23934  ptcn  23939  cnmpt11  23975  cnmpt1t  23977  cnmpt12  23979  cnmptkp  23992  cnmptk1  23993  cnmptkk  23995  cnmptk1p  23997  cnmptk2  23998  cnmpt1plusg  24399  cnmpt1vsca  24506  cnmpt1ds  25155  cncfcompt2  25222  cncfmpt2ss  25230  cnmpt1ip  25561  divcncf  25761  mbfmptcl  25950  i1fposd  26021  itgss3  26128  dvmptcl  26272  dvmptco  26285  dvle  26320  dvfsumle  26334  dvfsumge  26335  dvmptrecl  26337  itgparts  26360  itgsubstlem  26361  itgsubst  26362  ulmss  26717  ulmdvlem2  26721  itgulm2  26729  logtayl  26981  intlewftc  43091  cncfcompt  46862  cncficcgt0  46867  itgsubsticclem  46954  sge0iunmptlemre  47394  hoicvrrex  47535  smfadd  47744  smfpimioompt  47765