Theorem fvmpt3i 6941

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3431   ↦ cmpt 5153  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493

This theorem is referenced by:  isf32lem9  10274  axcc2lem  10349  caucvg  15632  ismre  17543  mrisval  17587  frmdup1  18823  frmdup2  18824  qusghm  19221  pmtrfval  19416  odf1  19528  vrgpfval  19732  dprdz  19998  dmdprdsplitlem  20005  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  ablfac1a  20037  ablfac1b  20038  ablfac1eu  20041  ipdir  21614  ipass  21620  isphld  21629  istopon  22895  qustgpopn  24103  qustgplem  24104  tcphcph  25222  cmvth  25976  mvth  25977  dvle  25992  lhop1  25999  dvfsumlem3  26013  pige3ALT  26502  fsumdvdscom  27166  logfacbnd3  27204  dchrptlem1  27245  dchrptlem2  27246  lgsdchrval  27335  dchrisumlem3  27472  dchrisum0flblem1  27489  dchrisum0fno1  27492  dchrisum0lem1b  27496  dchrisum0lem2a  27498  dchrisum0lem2  27499  logsqvma2  27524  log2sumbnd  27525  zringfrac  33637  measdivcst  34408  measdivcstALTV  34409  mrexval  35729  mexval  35730  mdvval  35732  msubvrs  35788  mthmval  35803  weiunlem  36691  f1omptsnlem  37698  upixp  38096  ismrer1  38205  frlmsnic  43026  fsuppind  43040  uzmptshftfval  44790  tposideq  49378  fucocolem2  49844  amgmwlem  50292  amgmlemALT  50293