Theorem fvmptelrn 6881

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
fvmptelrn.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)

Assertion

Ref	Expression
fvmptelrn	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem fvmptelrn

Step	Hyp	Ref	Expression
1		fvmptelrn.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
2		eqid 2738	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	fmpt 6878	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶𝐶)
4	1, 3	sylibr 237	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐶)
5	4	r19.21bi 3120	1 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2113  ∀wral 3053   ↦ cmpt 5107  ⟶wf 6329

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-fun 6335  df-fn 6336  df-f 6337

This theorem is referenced by:  rlimmptrcl  15048  lo1mptrcl  15062  o1mptrcl  15063  frlmgsum  20581  uvcresum  20602  psrass1lemOLD  20746  psrass1lem  20749  txcnp  22364  ptcnp  22366  ptcn  22371  cnmpt11  22407  cnmpt1t  22409  cnmpt12  22411  cnmptkp  22424  cnmptk1  22425  cnmptkk  22427  cnmptk1p  22429  cnmptk2  22430  cnmpt1plusg  22831  cnmpt1vsca  22938  cnmpt1ds  23587  cncfcompt2  23653  cncfmpt2ss  23661  cnmpt1ip  23992  divcncf  24192  mbfmptcl  24381  i1fposd  24452  itgss3  24559  dvmptcl  24703  dvmptco  24716  dvle  24751  dvfsumle  24765  dvfsumge  24766  dvmptrecl  24768  itgparts  24791  itgsubstlem  24792  itgsubst  24793  ulmss  25136  ulmdvlem2  25140  itgulm2  25148  logtayl  25395  intlewftc  39678  cncfcompt  42950  cncficcgt0  42955  itgsubsticclem  43042  sge0iunmptlemre  43479  hoicvrrex  43620  smfadd  43823  smfpimioompt  43843  smfsupmpt  43871  smfinfmpt  43875