Theorem fvmptelcdm 7060

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 7057	. . 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 6489

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 5232  ax-pr 5371

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 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-fun 6495  df-fn 6496  df-f 6497

This theorem is referenced by:  rlimmptrcl  15564  lo1mptrcl  15578  o1mptrcl  15579  frlmgsum  21765  uvcresum  21786  psrass1lem  21925  txcnp  23598  ptcnp  23600  ptcn  23605  cnmpt11  23641  cnmpt1t  23643  cnmpt12  23645  cnmptkp  23658  cnmptk1  23659  cnmptkk  23661  cnmptk1p  23663  cnmptk2  23664  cnmpt1plusg  24065  cnmpt1vsca  24172  cnmpt1ds  24821  cncfcompt2  24888  cncfmpt2ss  24896  cnmpt1ip  25227  divcncf  25427  mbfmptcl  25616  i1fposd  25687  itgss3  25795  dvmptcl  25939  dvmptco  25952  dvle  25987  dvfsumle  26001  dvfsumge  26002  dvmptrecl  26004  itgparts  26027  itgsubstlem  26028  itgsubst  26029  ulmss  26378  ulmdvlem2  26382  itgulm2  26390  logtayl  26640  intlewftc  42517  cncfcompt  46332  cncficcgt0  46337  itgsubsticclem  46424  sge0iunmptlemre  46864  hoicvrrex  47005  smfadd  47214  smfpimioompt  47235