Theorem fvmpt3i 6992

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ↦ cmpt 5186  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541

This theorem is used by:  isf32lem9  10363  axcc2lem  10438  caucvg  15766  ismre  17674  mrisval  17718  frmdup1  18973  frmdup2  18974  qusghm  19382  pmtrfval  19577  odf1  19689  vrgpfval  19893  dprdz  20159  dmdprdsplitlem  20166  dprd2dlem2  20169  dprd2dlem1  20170  dprd2da  20171  ablfac1a  20198  ablfac1b  20199  ablfac1eu  20202  ipdir  21852  ipass  21858  isphld  21867  istopon  23137  qustgpopn  24346  qustgplem  24347  tcphcph  25465  cmvth  26218  mvth  26219  dvle  26234  lhop1  26241  dvfsumlem3  26255  pige3ALT  26757  fsumdvdscom  27421  logfacbnd3  27459  dchrptlem1  27500  dchrptlem2  27501  lgsdchrval  27590  dchrisumlem3  27727  dchrisum0flblem1  27744  dchrisum0fno1  27747  dchrisum0lem1b  27751  dchrisum0lem2a  27753  dchrisum0lem2  27754  logsqvma2  27779  log2sumbnd  27780  zringfrac  33964  measdivcst  34735  measdivcstALTV  34736  mrexval  36080  mexval  36081  mdvval  36083  msubvrs  36139  mthmval  36154  weiunlem  37082  f1omptsnlem  38090  upixp  38479  ismrer1  38588  frlmsnic  43422  fsuppind  43436  uzmptshftfval  45170  tposideq  49814  fucocolem2  50280  veronesevald  50804  veronesevrowd  50812  amgmwlem  50820  amgmlemALT  50821