Theorem fvmpt3i 6859

Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.)

Hypotheses

Ref	Expression
fvmpt3.a	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmpt3.b	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmpt3i.c	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
fvmpt3i	⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

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

Proof of Theorem fvmpt3i

Step	Hyp	Ref	Expression
1		fvmpt3.a	. 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
2		fvmpt3.b	. 2 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
3		fvmpt3i.c	. . 3 ⊢ 𝐵 ∈ V
4	3	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ V)
5	1, 2, 4	fvmpt3 6858	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  Vcvv 3423   ↦ cmpt 5152  ‘cfv 6415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5479  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-iota 6373  df-fun 6417  df-fv 6423

This theorem is referenced by:  isf32lem9  10023  axcc2lem  10098  caucvg  15293  ismre  17191  mrisval  17231  frmdup1  18393  frmdup2  18394  qusghm  18761  pmtrfval  18948  odf1  19059  vrgpfval  19262  dprdz  19523  dmdprdsplitlem  19530  dprd2dlem2  19533  dprd2dlem1  19534  dprd2da  19535  ablfac1a  19562  ablfac1b  19563  ablfac1eu  19566  ipdir  20731  ipass  20737  isphld  20746  istopon  21944  qustgpopn  23154  qustgplem  23155  tcphcph  24281  cmvth  25035  mvth  25036  dvle  25051  lhop1  25058  dvfsumlem3  25072  pige3ALT  25556  fsumdvdscom  26214  logfacbnd3  26251  dchrptlem1  26292  dchrptlem2  26293  lgsdchrval  26382  dchrisumlem3  26519  dchrisum0flblem1  26536  dchrisum0fno1  26539  dchrisum0lem1b  26543  dchrisum0lem2a  26545  dchrisum0lem2  26546  logsqvma2  26571  log2sumbnd  26572  measdivcst  32067  measdivcstALTV  32068  mrexval  33338  mexval  33339  mdvval  33341  msubvrs  33397  mthmval  33412  f1omptsnlem  35413  upixp  35793  ismrer1  35902  frlmsnic  40160  fsuppind  40174  uzmptshftfval  41826  amgmwlem  46365  amgmlemALT  46366