Theorem fvmpt3i 6935

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ↦ cmpt 5173  ‘cfv 6482

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6438  df-fun 6484  df-fv 6490

This theorem is referenced by:  isf32lem9  10255  axcc2lem  10330  caucvg  15586  ismre  17492  mrisval  17536  frmdup1  18738  frmdup2  18739  qusghm  19134  pmtrfval  19329  odf1  19441  vrgpfval  19645  dprdz  19911  dmdprdsplitlem  19918  dprd2dlem2  19921  dprd2dlem1  19922  dprd2da  19923  ablfac1a  19950  ablfac1b  19951  ablfac1eu  19954  ipdir  21546  ipass  21552  isphld  21561  istopon  22797  qustgpopn  24005  qustgplem  24006  tcphcph  25135  cmvth  25893  cmvthOLD  25894  mvth  25895  dvle  25910  lhop1  25917  dvfsumlem3  25933  pige3ALT  26427  fsumdvdscom  27093  logfacbnd3  27132  dchrptlem1  27173  dchrptlem2  27174  lgsdchrval  27263  dchrisumlem3  27400  dchrisum0flblem1  27417  dchrisum0fno1  27420  dchrisum0lem1b  27424  dchrisum0lem2a  27426  dchrisum0lem2  27427  logsqvma2  27452  log2sumbnd  27453  zringfrac  33491  measdivcst  34191  measdivcstALTV  34192  mrexval  35474  mexval  35475  mdvval  35477  msubvrs  35533  mthmval  35548  weiunlem2  36437  f1omptsnlem  37310  upixp  37709  ismrer1  37818  frlmsnic  42513  fsuppind  42563  uzmptshftfval  44319  tposideq  48872  fucocolem2  49339  amgmwlem  49787  amgmlemALT  49788