MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fvmpt3i Structured version   Unicode version

Theorem fvmpt3i 5773
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
StepHypRef 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
43a1i 11 . 2  |-  ( x  e.  D  ->  B  e.  _V )
51, 2, 4fvmpt3 5772 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   _Vcvv 2967    e. cmpt 4345   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-iota 5376  df-fun 5415  df-fv 5421
This theorem is referenced by:  isf32lem9  8522  axcc2lem  8597  caucvg  13148  ismre  14520  mrisval  14560  frmdup1  15533  frmdup2  15534  divsghm  15774  pmtrfval  15947  odf1  16054  vrgpfval  16254  dprdz  16517  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dprd2dlem2  16529  dprd2dlem1  16530  dprd2da  16531  ablfac1a  16560  ablfac1b  16561  ablfac1eu  16564  ipdir  18048  ipass  18054  isphld  18063  istopon  18510  divstgpopn  19670  divstgplem  19671  tchcph  20732  cmvth  21443  mvth  21444  dvle  21459  lhop1  21466  dvfsumlem3  21480  pige3  21959  fsumdvdscom  22505  logfacbnd3  22542  dchrptlem1  22583  dchrptlem2  22584  lgsdchrval  22666  dchrisumlem3  22720  dchrisum0flblem1  22737  dchrisum0fno1  22740  dchrisum0lem1b  22744  dchrisum0lem2a  22746  dchrisum0lem2  22747  logsqvma2  22772  log2sumbnd  22773  measdivcstOLD  26607  measdivcst  26608  upixp  28594  ismrer1  28708
  Copyright terms: Public domain W3C validator