Theorem fvmpt3i 7004

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ↦ cmpt 5185  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fv 6551

This theorem is used by:  isf32lem9  10446  axcc2lem  10521  caucvg  15855  ismre  17769  mrisval  17813  frmdup1  19069  frmdup2  19070  qusghm  19478  pmtrfval  19673  odf1  19785  vrgpfval  19989  dprdz  20255  dmdprdsplitlem  20262  dprd2dlem2  20265  dprd2dlem1  20266  dprd2da  20267  ablfac1a  20294  ablfac1b  20295  ablfac1eu  20298  ipdir  21954  ipass  21960  isphld  21969  istopon  23239  qustgpopn  24448  qustgplem  24449  tcphcph  25567  cmvth  26320  mvth  26321  dvle  26336  lhop1  26343  dvfsumlem3  26357  pige3ALT  26857  fsumdvdscom  27521  logfacbnd3  27559  dchrptlem1  27600  dchrptlem2  27601  lgsdchrval  27690  dchrisumlem3  27827  dchrisum0flblem1  27844  dchrisum0fno1  27847  dchrisum0lem1b  27851  dchrisum0lem2a  27853  dchrisum0lem2  27854  logsqvma2  27879  log2sumbnd  27880  zringfrac  34136  measdivcst  34907  measdivcstALTV  34908  mrexval  36356  mexval  36357  mdvval  36359  msubvrs  36415  mthmval  36430  weiunlem  37347  f1omptsnlem  38368  upixp  38772  ismrer1  38881  frlmsnic  43713  fsuppind  43727  uzmptshftfval  45439  tposideq  50109  fucocolem2  50584  veronesevald  51154  veronesevrowd  51162  amgmwlem  51170  amgmlemALT  51171