Theorem fvmpt3i 6955

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ↦ cmpt 5183  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507

This theorem is referenced by:  isf32lem9  10290  axcc2lem  10365  caucvg  15621  ismre  17527  mrisval  17567  frmdup1  18767  frmdup2  18768  qusghm  19163  pmtrfval  19356  odf1  19468  vrgpfval  19672  dprdz  19938  dmdprdsplitlem  19945  dprd2dlem2  19948  dprd2dlem1  19949  dprd2da  19950  ablfac1a  19977  ablfac1b  19978  ablfac1eu  19981  ipdir  21524  ipass  21530  isphld  21539  istopon  22775  qustgpopn  23983  qustgplem  23984  tcphcph  25113  cmvth  25871  cmvthOLD  25872  mvth  25873  dvle  25888  lhop1  25895  dvfsumlem3  25911  pige3ALT  26405  fsumdvdscom  27071  logfacbnd3  27110  dchrptlem1  27151  dchrptlem2  27152  lgsdchrval  27241  dchrisumlem3  27378  dchrisum0flblem1  27395  dchrisum0fno1  27398  dchrisum0lem1b  27402  dchrisum0lem2a  27404  dchrisum0lem2  27405  logsqvma2  27430  log2sumbnd  27431  zringfrac  33498  measdivcst  34187  measdivcstALTV  34188  mrexval  35461  mexval  35462  mdvval  35464  msubvrs  35520  mthmval  35535  weiunlem2  36424  f1omptsnlem  37297  upixp  37696  ismrer1  37805  frlmsnic  42501  fsuppind  42551  uzmptshftfval  44308  tposideq  48849  fucocolem2  49316  amgmwlem  49764  amgmlemALT  49765