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

Theorem fvmpt3i 5877
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 5876 1  |-  ( A  e.  D  ->  ( F `  A )  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    e. wcel 1758   _Vcvv 3068    |-> cmpt 4448   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524
This theorem is referenced by:  isf32lem9  8631  axcc2lem  8706  caucvg  13258  ismre  14630  mrisval  14670  frmdup1  15644  frmdup2  15645  divsghm  15885  pmtrfval  16058  odf1  16167  vrgpfval  16367  dprdz  16632  dmdprdsplitlem  16639  dmdprdsplitlemOLD  16640  dprd2dlem2  16644  dprd2dlem1  16645  dprd2da  16646  ablfac1a  16675  ablfac1b  16676  ablfac1eu  16679  ipdir  18177  ipass  18183  isphld  18192  istopon  18646  divstgpopn  19806  divstgplem  19807  tchcph  20868  cmvth  21579  mvth  21580  dvle  21595  lhop1  21602  dvfsumlem3  21616  pige3  22095  fsumdvdscom  22641  logfacbnd3  22678  dchrptlem1  22719  dchrptlem2  22720  lgsdchrval  22802  dchrisumlem3  22856  dchrisum0flblem1  22873  dchrisum0fno1  22876  dchrisum0lem1b  22880  dchrisum0lem2a  22882  dchrisum0lem2  22883  logsqvma2  22908  log2sumbnd  22909  measdivcstOLD  26772  measdivcst  26773  upixp  28761  ismrer1  28875
  Copyright terms: Public domain W3C validator