Theorem fvmptelcdm 7114

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061   ↦ cmpt 5231  ⟶wf 6539

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  rlimmptrcl  15554  lo1mptrcl  15568  o1mptrcl  15569  frlmgsum  21333  uvcresum  21354  psrass1lemOLD  21499  psrass1lem  21502  txcnp  23131  ptcnp  23133  ptcn  23138  cnmpt11  23174  cnmpt1t  23176  cnmpt12  23178  cnmptkp  23191  cnmptk1  23192  cnmptkk  23194  cnmptk1p  23196  cnmptk2  23197  cnmpt1plusg  23598  cnmpt1vsca  23705  cnmpt1ds  24365  cncfcompt2  24431  cncfmpt2ss  24439  cnmpt1ip  24771  divcncf  24971  mbfmptcl  25160  i1fposd  25232  itgss3  25339  dvmptcl  25483  dvmptco  25496  dvle  25531  dvfsumle  25545  dvfsumge  25546  dvmptrecl  25548  itgparts  25571  itgsubstlem  25572  itgsubst  25573  ulmss  25916  ulmdvlem2  25920  itgulm2  25928  logtayl  26175  gg-dvfsumle  35251  intlewftc  41012  cncfcompt  44678  cncficcgt0  44683  itgsubsticclem  44770  sge0iunmptlemre  45210  hoicvrrex  45351  smfadd  45560  smfpimioompt  45581  smfinfmpt  45614