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

Theorem fvmpts 5760
 Description: Value of a function given in maps-to notation, using explicit class substitution. (Contributed by Scott Fenton, 17-Jul-2013.) (Revised by Mario Carneiro, 31-Aug-2015.)
Hypothesis
Ref Expression
fvmpts.1
Assertion
Ref Expression
fvmpts
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem fvmpts
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 csbeq1 3211 . 2
2 fvmpts.1 . . 3
3 nfcv 2537 . . . 4
4 nfcsb1v 3240 . . . 4
5 csbeq1a 3216 . . . 4
63, 4, 5cbvmpt 4254 . . 3
72, 6eqtri 2421 . 2
81, 7fvmptg 5757 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wceq 1649   wcel 1721  csb 3208   cmpt 4221  cfv 5408 This theorem is referenced by:  fvmptd  5763  pcmpt  13202  issubc  13976  prdsdsf  18336  itgparts  19870  dchrisumlema  21121  abfmpeld  23986  abfmpel  23987  prodss  25195  fprodser  25197  fprodefsum  25220  fprodn0  25225  aomclem6  26986  cdlemk40  31339 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-sep 4285  ax-nul 4293  ax-pr 4358 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-ral 2668  df-rex 2669  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-nul 3586  df-if 3697  df-sn 3777  df-pr 3778  df-op 3780  df-uni 3972  df-br 4168  df-opab 4222  df-mpt 4223  df-id 4453  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-iota 5372  df-fun 5410  df-fv 5416
 Copyright terms: Public domain W3C validator