Theorem fvmptelcdm 7112

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3081   ↦ cmpt 5194  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-fun 6542  df-fn 6543  df-f 6544

This theorem is used by:  rlimmptrcl  15683  lo1mptrcl  15697  o1mptrcl  15698  frlmgsum  21972  uvcresum  21993  psrass1lem  22133  txcnp  23828  ptcnp  23830  ptcn  23835  cnmpt11  23871  cnmpt1t  23873  cnmpt12  23875  cnmptkp  23888  cnmptk1  23889  cnmptkk  23891  cnmptk1p  23893  cnmptk2  23894  cnmpt1plusg  24295  cnmpt1vsca  24402  cnmpt1ds  25051  cncfcompt2  25118  cncfmpt2ss  25126  cnmpt1ip  25457  divcncf  25657  mbfmptcl  25846  i1fposd  25917  itgss3  26025  dvmptcl  26169  dvmptco  26182  dvle  26217  dvfsumle  26231  dvfsumge  26232  dvmptrecl  26234  itgparts  26257  itgsubstlem  26258  itgsubst  26259  ulmss  26611  ulmdvlem2  26615  itgulm2  26623  logtayl  26876  intlewftc  42886  cncfcompt  46655  cncficcgt0  46660  itgsubsticclem  46747  sge0iunmptlemre  47187  hoicvrrex  47328  smfadd  47537  smfpimioompt  47558