Theorem fvmptelcdm 7019

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  ∀wral 3061   ↦ cmpt 5164  ⟶wf 6454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3333  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-fun 6460  df-fn 6461  df-f 6462

This theorem is referenced by:  rlimmptrcl  15366  lo1mptrcl  15380  o1mptrcl  15381  frlmgsum  21028  uvcresum  21049  psrass1lemOLD  21192  psrass1lem  21195  txcnp  22820  ptcnp  22822  ptcn  22827  cnmpt11  22863  cnmpt1t  22865  cnmpt12  22867  cnmptkp  22880  cnmptk1  22881  cnmptkk  22883  cnmptk1p  22885  cnmptk2  22886  cnmpt1plusg  23287  cnmpt1vsca  23394  cnmpt1ds  24054  cncfcompt2  24120  cncfmpt2ss  24128  cnmpt1ip  24460  divcncf  24660  mbfmptcl  24849  i1fposd  24921  itgss3  25028  dvmptcl  25172  dvmptco  25185  dvle  25220  dvfsumle  25234  dvfsumge  25235  dvmptrecl  25237  itgparts  25260  itgsubstlem  25261  itgsubst  25262  ulmss  25605  ulmdvlem2  25609  itgulm2  25617  logtayl  25864  intlewftc  40269  cncfcompt  43653  cncficcgt0  43658  itgsubsticclem  43745  sge0iunmptlemre  44183  hoicvrrex  44324  smfadd  44533  smfpimioompt  44554  smfinfmpt  44587