Theorem fvmptelcdm 7097

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3060   ↦ cmpt 5224  ⟶wf 6528

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 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420

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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-fun 6534  df-fn 6535  df-f 6536

This theorem is referenced by:  rlimmptrcl  15534  lo1mptrcl  15548  o1mptrcl  15549  frlmgsum  21260  uvcresum  21281  psrass1lemOLD  21424  psrass1lem  21427  txcnp  23053  ptcnp  23055  ptcn  23060  cnmpt11  23096  cnmpt1t  23098  cnmpt12  23100  cnmptkp  23113  cnmptk1  23114  cnmptkk  23116  cnmptk1p  23118  cnmptk2  23119  cnmpt1plusg  23520  cnmpt1vsca  23627  cnmpt1ds  24287  cncfcompt2  24353  cncfmpt2ss  24361  cnmpt1ip  24693  divcncf  24893  mbfmptcl  25082  i1fposd  25154  itgss3  25261  dvmptcl  25405  dvmptco  25418  dvle  25453  dvfsumle  25467  dvfsumge  25468  dvmptrecl  25470  itgparts  25493  itgsubstlem  25494  itgsubst  25495  ulmss  25838  ulmdvlem2  25842  itgulm2  25850  logtayl  26097  intlewftc  40729  cncfcompt  44370  cncficcgt0  44375  itgsubsticclem  44462  sge0iunmptlemre  44902  hoicvrrex  45043  smfadd  45252  smfpimioompt  45273  smfinfmpt  45306