Theorem fvmpt3i 6995

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ↦ cmpt 5192  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544

This theorem is referenced by:  isf32lem9  10340  axcc2lem  10415  caucvg  15726  ismre  17637  mrisval  17681  frmdup1  18918  frmdup2  18919  qusghm  19320  pmtrfval  19515  odf1  19627  vrgpfval  19831  dprdz  20097  dmdprdsplitlem  20104  dprd2dlem2  20107  dprd2dlem1  20108  dprd2da  20109  ablfac1a  20136  ablfac1b  20137  ablfac1eu  20140  ipdir  21789  ipass  21795  isphld  21804  istopon  23069  qustgpopn  24277  qustgplem  24278  tcphcph  25396  cmvth  26150  mvth  26151  dvle  26166  lhop1  26173  dvfsumlem3  26187  pige3ALT  26685  fsumdvdscom  27349  logfacbnd3  27387  dchrptlem1  27428  dchrptlem2  27429  lgsdchrval  27518  dchrisumlem3  27655  dchrisum0flblem1  27672  dchrisum0fno1  27675  dchrisum0lem1b  27679  dchrisum0lem2a  27681  dchrisum0lem2  27682  logsqvma2  27707  log2sumbnd  27708  zringfrac  33844  measdivcst  34614  measdivcstALTV  34615  mrexval  35993  mexval  35994  mdvval  35996  msubvrs  36052  mthmval  36067  weiunlem  36974  f1omptsnlem  37982  upixp  38380  ismrer1  38489  frlmsnic  43308  fsuppind  43322  uzmptshftfval  45056  tposideq  49666  fucocolem2  50132  amgmwlem  50622  amgmlemALT  50623