Theorem fvmpt3i 7021

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ↦ cmpt 5225  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  isf32lem9  10401  axcc2lem  10476  caucvg  15715  ismre  17633  mrisval  17673  frmdup1  18877  frmdup2  18878  qusghm  19273  pmtrfval  19468  odf1  19580  vrgpfval  19784  dprdz  20050  dmdprdsplitlem  20057  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  ablfac1a  20089  ablfac1b  20090  ablfac1eu  20093  ipdir  21657  ipass  21663  isphld  21672  istopon  22918  qustgpopn  24128  qustgplem  24129  tcphcph  25271  cmvth  26029  cmvthOLD  26030  mvth  26031  dvle  26046  lhop1  26053  dvfsumlem3  26069  pige3ALT  26562  fsumdvdscom  27228  logfacbnd3  27267  dchrptlem1  27308  dchrptlem2  27309  lgsdchrval  27398  dchrisumlem3  27535  dchrisum0flblem1  27552  dchrisum0fno1  27555  dchrisum0lem1b  27559  dchrisum0lem2a  27561  dchrisum0lem2  27562  logsqvma2  27587  log2sumbnd  27588  zringfrac  33582  measdivcst  34225  measdivcstALTV  34226  mrexval  35506  mexval  35507  mdvval  35509  msubvrs  35565  mthmval  35580  weiunlem2  36464  f1omptsnlem  37337  upixp  37736  ismrer1  37845  frlmsnic  42550  fsuppind  42600  uzmptshftfval  44365  tposideq  48788  fucocolem2  49049  amgmwlem  49321  amgmlemALT  49322