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

Theorem fvmpt3i 6180
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
StepHypRef Expression
1 fvmpt3.a . 2 (𝑥 = 𝐴𝐵 = 𝐶)
2 fvmpt3.b . 2 𝐹 = (𝑥𝐷𝐵)
3 fvmpt3i.c . . 3 𝐵 ∈ V
43a1i 11 . 2 (𝑥𝐷𝐵 ∈ V)
51, 2, 4fvmpt3 6179 1 (𝐴𝐷 → (𝐹𝐴) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976  Vcvv 3172  cmpt 4637  cfv 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4942  df-xp 5033  df-rel 5034  df-cnv 5035  df-co 5036  df-dm 5037  df-iota 5753  df-fun 5791  df-fv 5797
This theorem is referenced by:  isf32lem9  9043  axcc2lem  9118  caucvg  14205  ismre  16021  mrisval  16061  frmdup1  17172  frmdup2  17173  qusghm  17468  pmtrfval  17641  odf1  17750  vrgpfval  17950  dprdz  18200  dmdprdsplitlem  18207  dprd2dlem2  18210  dprd2dlem1  18211  dprd2da  18212  ablfac1a  18239  ablfac1b  18240  ablfac1eu  18243  ipdir  19750  ipass  19756  isphld  19765  istopon  20487  qustgpopn  21680  qustgplem  21681  tchcph  22788  cmvth  23502  mvth  23503  dvle  23518  lhop1  23525  dvfsumlem3  23539  pige3  24017  fsumdvdscom  24655  logfacbnd3  24692  dchrptlem1  24733  dchrptlem2  24734  lgsdchrval  24823  dchrisumlem3  24924  dchrisum0flblem1  24941  dchrisum0fno1  24944  dchrisum0lem1b  24948  dchrisum0lem2a  24950  dchrisum0lem2  24951  logsqvma2  24976  log2sumbnd  24977  sgnsv  28851  measdivcstOLD  29407  measdivcst  29408  mrexval  30445  mexval  30446  mdvval  30448  msubvrs  30504  mthmval  30519  f1omptsnlem  32142  upixp  32477  ismrer1  32590  uzmptshftfval  37350  amgmwlem  42299  amgmlemALT  42300
  Copyright terms: Public domain W3C validator