Theorem fvmpt3i 6981

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 6980	1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ↦ cmpt 5181  ‘cfv 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6477  df-fun 6523  df-fv 6529

This theorem is referenced by:  isf32lem9  10318  axcc2lem  10393  caucvg  15706  ismre  17618  mrisval  17662  frmdup1  18898  frmdup2  18899  qusghm  19295  pmtrfval  19490  odf1  19602  vrgpfval  19806  dprdz  20072  dmdprdsplitlem  20079  dprd2dlem2  20082  dprd2dlem1  20083  dprd2da  20084  ablfac1a  20111  ablfac1b  20112  ablfac1eu  20115  ipdir  21688  ipass  21694  isphld  21703  istopon  22969  qustgpopn  24177  qustgplem  24178  tcphcph  25296  cmvth  26050  mvth  26051  dvle  26066  lhop1  26073  dvfsumlem3  26087  pige3ALT  26582  fsumdvdscom  27246  logfacbnd3  27284  dchrptlem1  27325  dchrptlem2  27326  lgsdchrval  27415  dchrisumlem3  27552  dchrisum0flblem1  27569  dchrisum0fno1  27572  dchrisum0lem1b  27576  dchrisum0lem2a  27578  dchrisum0lem2  27579  logsqvma2  27604  log2sumbnd  27605  zringfrac  33747  measdivcst  34518  measdivcstALTV  34519  mrexval  35848  mexval  35849  mdvval  35851  msubvrs  35907  mthmval  35922  weiunlem  36820  f1omptsnlem  37827  upixp  38225  ismrer1  38334  frlmsnic  43155  fsuppind  43169  uzmptshftfval  44919  tposideq  49506  fucocolem2  49972  amgmwlem  50420  amgmlemALT  50421