Theorem fvmpt3i 6946

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  isf32lem9  10271  axcc2lem  10346  caucvg  15602  ismre  17509  mrisval  17553  frmdup1  18789  frmdup2  18790  qusghm  19184  pmtrfval  19379  odf1  19491  vrgpfval  19695  dprdz  19961  dmdprdsplitlem  19968  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  ablfac1a  20000  ablfac1b  20001  ablfac1eu  20004  ipdir  21594  ipass  21600  isphld  21609  istopon  22856  qustgpopn  24064  qustgplem  24065  tcphcph  25193  cmvth  25951  cmvthOLD  25952  mvth  25953  dvle  25968  lhop1  25975  dvfsumlem3  25991  pige3ALT  26485  fsumdvdscom  27151  logfacbnd3  27190  dchrptlem1  27231  dchrptlem2  27232  lgsdchrval  27321  dchrisumlem3  27458  dchrisum0flblem1  27475  dchrisum0fno1  27478  dchrisum0lem1b  27482  dchrisum0lem2a  27484  dchrisum0lem2  27485  logsqvma2  27510  log2sumbnd  27511  zringfrac  33635  measdivcst  34381  measdivcstALTV  34382  mrexval  35695  mexval  35696  mdvval  35698  msubvrs  35754  mthmval  35769  weiunlem  36657  f1omptsnlem  37541  upixp  37930  ismrer1  38039  frlmsnic  42795  fsuppind  42833  uzmptshftfval  44587  tposideq  49133  fucocolem2  49599  amgmwlem  50047  amgmlemALT  50048