Theorem fvmpt3i 7030

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ↦ cmpt 5192  ‘cfv 6566

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574

This theorem is used by:  isf32lem9  10478  axcc2lem  10553  caucvg  15890  ismre  17810  mrisval  17854  frmdup1  19110  frmdup2  19111  qusghm  19519  pmtrfval  19715  odf1  19827  vrgpfval  20031  dprdz  20297  dmdprdsplitlem  20304  dprd2dlem2  20307  dprd2dlem1  20308  dprd2da  20309  ablfac1a  20336  ablfac1b  20337  ablfac1eu  20340  ipdir  22000  ipass  22006  isphld  22015  istopon  23285  qustgpopn  24494  qustgplem  24495  tcphcph  25613  cmvth  26366  mvth  26367  dvle  26382  lhop1  26389  dvfsumlem3  26403  pige3ALT  26905  fsumdvdscom  27569  logfacbnd3  27607  dchrptlem1  27648  dchrptlem2  27649  lgsdchrval  27738  dchrisumlem3  27875  dchrisum0flblem1  27892  dchrisum0fno1  27895  dchrisum0lem1b  27899  dchrisum0lem2a  27901  dchrisum0lem2  27902  logsqvma2  27927  log2sumbnd  27928  zringfrac  34189  measdivcst  34968  measdivcstALTV  34969  mrexval  36474  mexval  36475  mdvval  36477  msubvrs  36533  mthmval  36548  weiunlem  37466  f1omptsnlem  38527  upixp  38931  ismrer1  39038  frlmsnic  43870  fsuppind  43884  uzmptshftfval  45591  tposideq  50332  fucocolem2  50807  veronesevald  51399  veronesevrowd  51407  amgmwlem  51415  amgmlemALT  51416