Theorem fvmptelcdm 7102

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3051   ↦ cmpt 5201  ⟶wf 6526

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6532  df-fn 6533  df-f 6534

This theorem is referenced by:  rlimmptrcl  15622  lo1mptrcl  15636  o1mptrcl  15637  frlmgsum  21730  uvcresum  21751  psrass1lem  21890  txcnp  23556  ptcnp  23558  ptcn  23563  cnmpt11  23599  cnmpt1t  23601  cnmpt12  23603  cnmptkp  23616  cnmptk1  23617  cnmptkk  23619  cnmptk1p  23621  cnmptk2  23622  cnmpt1plusg  24023  cnmpt1vsca  24130  cnmpt1ds  24780  cncfcompt2  24850  cncfmpt2ss  24858  cnmpt1ip  25197  divcncf  25398  mbfmptcl  25587  i1fposd  25658  itgss3  25766  dvmptcl  25913  dvmptco  25926  dvle  25962  dvfsumle  25976  dvfsumleOLD  25977  dvfsumge  25978  dvmptrecl  25980  itgparts  26004  itgsubstlem  26005  itgsubst  26006  ulmss  26356  ulmdvlem2  26360  itgulm2  26368  logtayl  26619  intlewftc  42020  cncfcompt  45860  cncficcgt0  45865  itgsubsticclem  45952  sge0iunmptlemre  46392  hoicvrrex  46533  smfadd  46742  smfpimioompt  46763