Theorem fvmpt3i 6534

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

Syntax hints:   → wi 4   = wceq 1658   ∈ wcel 2166  Vcvv 3414   ↦ cmpt 4952  ‘cfv 6123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-iota 6086  df-fun 6125  df-fv 6131

This theorem is referenced by:  isf32lem9  9498  axcc2lem  9573  caucvg  14786  ismre  16603  mrisval  16643  frmdup1  17755  frmdup2  17756  qusghm  18048  pmtrfval  18220  odf1  18330  vrgpfval  18532  dprdz  18783  dmdprdsplitlem  18790  dprd2dlem2  18793  dprd2dlem1  18794  dprd2da  18795  ablfac1a  18822  ablfac1b  18823  ablfac1eu  18826  ipdir  20346  ipass  20352  isphld  20361  istopon  21087  qustgpopn  22293  qustgplem  22294  tcphcph  23405  cmvth  24153  mvth  24154  dvle  24169  lhop1  24176  dvfsumlem3  24190  pige3  24669  fsumdvdscom  25324  logfacbnd3  25361  dchrptlem1  25402  dchrptlem2  25403  lgsdchrval  25492  dchrisumlem3  25593  dchrisum0flblem1  25610  dchrisum0fno1  25613  dchrisum0lem1b  25617  dchrisum0lem2a  25619  dchrisum0lem2  25620  logsqvma2  25645  log2sumbnd  25646  measdivcstOLD  30832  measdivcst  30833  mrexval  31944  mexval  31945  mdvval  31947  msubvrs  32003  mthmval  32018  f1omptsnlem  33729  upixp  34067  ismrer1  34179  uzmptshftfval  39385  amgmwlem  43444  amgmlemALT  43445