Theorem fvmpt3i 6997

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  isf32lem9  10432  axcc2lem  10507  caucvg  15839  ismre  17753  mrisval  17797  frmdup1  19053  frmdup2  19054  qusghm  19462  pmtrfval  19657  odf1  19769  vrgpfval  19973  dprdz  20239  dmdprdsplitlem  20246  dprd2dlem2  20249  dprd2dlem1  20250  dprd2da  20251  ablfac1a  20278  ablfac1b  20279  ablfac1eu  20282  ipdir  21938  ipass  21944  isphld  21953  istopon  23223  qustgpopn  24432  qustgplem  24433  tcphcph  25551  cmvth  26304  mvth  26305  dvle  26320  lhop1  26327  dvfsumlem3  26341  pige3ALT  26841  fsumdvdscom  27505  logfacbnd3  27543  dchrptlem1  27584  dchrptlem2  27585  lgsdchrval  27674  dchrisumlem3  27811  dchrisum0flblem1  27828  dchrisum0fno1  27831  dchrisum0lem1b  27835  dchrisum0lem2a  27837  dchrisum0lem2  27838  logsqvma2  27863  log2sumbnd  27864  zringfrac  34079  measdivcst  34850  measdivcstALTV  34851  mrexval  36245  mexval  36246  mdvval  36248  msubvrs  36304  mthmval  36319  weiunlem  37231  f1omptsnlem  38239  upixp  38643  ismrer1  38752  frlmsnic  43584  fsuppind  43598  uzmptshftfval  45315  tposideq  49965  fucocolem2  50431  veronesevald  50940  veronesevrowd  50948  amgmwlem  50956  amgmlemALT  50957