Theorem fvmpt3i 6944

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3438   ↦ cmpt 5177  ‘cfv 6490

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-iota 6446  df-fun 6492  df-fv 6498

This theorem is referenced by:  isf32lem9  10269  axcc2lem  10344  caucvg  15600  ismre  17507  mrisval  17551  frmdup1  18787  frmdup2  18788  qusghm  19182  pmtrfval  19377  odf1  19489  vrgpfval  19693  dprdz  19959  dmdprdsplitlem  19966  dprd2dlem2  19969  dprd2dlem1  19970  dprd2da  19971  ablfac1a  19998  ablfac1b  19999  ablfac1eu  20002  ipdir  21592  ipass  21598  isphld  21607  istopon  22854  qustgpopn  24062  qustgplem  24063  tcphcph  25191  cmvth  25949  cmvthOLD  25950  mvth  25951  dvle  25966  lhop1  25973  dvfsumlem3  25989  pige3ALT  26483  fsumdvdscom  27149  logfacbnd3  27188  dchrptlem1  27229  dchrptlem2  27230  lgsdchrval  27319  dchrisumlem3  27456  dchrisum0flblem1  27473  dchrisum0fno1  27476  dchrisum0lem1b  27480  dchrisum0lem2a  27482  dchrisum0lem2  27483  logsqvma2  27508  log2sumbnd  27509  zringfrac  33584  measdivcst  34330  measdivcstALTV  34331  mrexval  35644  mexval  35645  mdvval  35647  msubvrs  35703  mthmval  35718  weiunlem2  36606  f1omptsnlem  37480  upixp  37869  ismrer1  37978  frlmsnic  42737  fsuppind  42775  uzmptshftfval  44529  tposideq  49075  fucocolem2  49541  amgmwlem  49989  amgmlemALT  49990