![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvmpt3i | Structured version Visualization version GIF version |
Description: Value of a function given in maps-to notation, with a slightly different sethood condition. (Contributed by Mario Carneiro, 11-Sep-2015.) |
Ref | Expression |
---|---|
fvmpt3.a | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
fvmpt3.b | ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) |
fvmpt3i.c | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
fvmpt3i | ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmpt3.a | . 2 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
2 | fvmpt3.b | . 2 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
3 | fvmpt3i.c | . . 3 ⊢ 𝐵 ∈ V | |
4 | 3 | a1i 11 | . 2 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ V) |
5 | 1, 2, 4 | fvmpt3 6749 | 1 ⊢ (𝐴 ∈ 𝐷 → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 Vcvv 3441 ↦ cmpt 5110 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 |
This theorem is referenced by: isf32lem9 9772 axcc2lem 9847 caucvg 15027 ismre 16853 mrisval 16893 frmdup1 18021 frmdup2 18022 qusghm 18387 pmtrfval 18570 odf1 18681 vrgpfval 18884 dprdz 19145 dmdprdsplitlem 19152 dprd2dlem2 19155 dprd2dlem1 19156 dprd2da 19157 ablfac1a 19184 ablfac1b 19185 ablfac1eu 19188 ipdir 20328 ipass 20334 isphld 20343 istopon 21517 qustgpopn 22725 qustgplem 22726 tcphcph 23841 cmvth 24594 mvth 24595 dvle 24610 lhop1 24617 dvfsumlem3 24631 pige3ALT 25112 fsumdvdscom 25770 logfacbnd3 25807 dchrptlem1 25848 dchrptlem2 25849 lgsdchrval 25938 dchrisumlem3 26075 dchrisum0flblem1 26092 dchrisum0fno1 26095 dchrisum0lem1b 26099 dchrisum0lem2a 26101 dchrisum0lem2 26102 logsqvma2 26127 log2sumbnd 26128 measdivcst 31593 measdivcstALTV 31594 mrexval 32861 mexval 32862 mdvval 32864 msubvrs 32920 mthmval 32935 f1omptsnlem 34753 upixp 35167 ismrer1 35276 frlmsnic 39453 fsuppind 39456 uzmptshftfval 41050 amgmwlem 45330 amgmlemALT 45331 |
Copyright terms: Public domain | W3C validator |