Theorem fvmpt3i 6287

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	|- ( x = A -> B = C )
fvmpt3.b	|- F = ( x e. D |-> B )
fvmpt3i.c	|- B e. _V

Assertion

Ref	Expression
fvmpt3i	|- ( A e. D -> ( F ` A ) = C )

Distinct variable groups:   x, A   x, C   x, D

Allowed substitution hints:   B( x)   F( x)

Proof of Theorem fvmpt3i

Step	Hyp	Ref	Expression
1		fvmpt3.a	. 2 |- ( x = A -> B = C )
2		fvmpt3.b	. 2 |- F = ( x e. D |-> B )
3		fvmpt3i.c	. . 3 |- B e. _V
4	3	a1i 11	. 2 |- ( x e. D -> B e. _V )
5	1, 2, 4	fvmpt3 6286	1 |- ( A e. D -> ( F ` A ) = C )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990   _Vcvv 3200   |-> cmpt 4729   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896

This theorem is referenced by:  isf32lem9  9183  axcc2lem  9258  caucvg  14409  ismre  16250  mrisval  16290  frmdup1  17401  frmdup2  17402  qusghm  17697  pmtrfval  17870  odf1  17979  vrgpfval  18179  dprdz  18429  dmdprdsplitlem  18436  dprd2dlem2  18439  dprd2dlem1  18440  dprd2da  18441  ablfac1a  18468  ablfac1b  18469  ablfac1eu  18472  ipdir  19984  ipass  19990  isphld  19999  istopon  20717  qustgpopn  21923  qustgplem  21924  tchcph  23036  cmvth  23754  mvth  23755  dvle  23770  lhop1  23777  dvfsumlem3  23791  pige3  24269  fsumdvdscom  24911  logfacbnd3  24948  dchrptlem1  24989  dchrptlem2  24990  lgsdchrval  25079  dchrisumlem3  25180  dchrisum0flblem1  25197  dchrisum0fno1  25200  dchrisum0lem1b  25204  dchrisum0lem2a  25206  dchrisum0lem2  25207  logsqvma2  25232  log2sumbnd  25233  sgnsv  29727  measdivcstOLD  30287  measdivcst  30288  mrexval  31398  mexval  31399  mdvval  31401  msubvrs  31457  mthmval  31472  f1omptsnlem  33183  upixp  33524  ismrer1  33637  uzmptshftfval  38545  amgmwlem  42548  amgmlemALT  42549