![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvmptf | Structured version Visualization version GIF version |
Description: Value of a function given by an ordered-pair class abstraction. This version of fvmptg 6743 uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 8-Nov-2005.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Ref | Expression |
---|---|
fvmptf.1 | ⊢ Ⅎ𝑥𝐴 |
fvmptf.2 | ⊢ Ⅎ𝑥𝐶 |
fvmptf.3 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
fvmptf.4 | ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) |
Ref | Expression |
---|---|
fvmptf | ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmptf.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
2 | fvmptf.2 | . . . . 5 ⊢ Ⅎ𝑥𝐶 | |
3 | 2 | nfel1 2971 | . . . 4 ⊢ Ⅎ𝑥 𝐶 ∈ V |
4 | fvmptf.4 | . . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
5 | nfmpt1 5128 | . . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐷 ↦ 𝐵) | |
6 | 4, 5 | nfcxfr 2953 | . . . . . 6 ⊢ Ⅎ𝑥𝐹 |
7 | 6, 1 | nffv 6655 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝐴) |
8 | 7, 2 | nfeq 2968 | . . . 4 ⊢ Ⅎ𝑥(𝐹‘𝐴) = 𝐶 |
9 | 3, 8 | nfim 1897 | . . 3 ⊢ Ⅎ𝑥(𝐶 ∈ V → (𝐹‘𝐴) = 𝐶) |
10 | fvmptf.3 | . . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
11 | 10 | eleq1d 2874 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V)) |
12 | fveq2 6645 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | |
13 | 12, 10 | eqeq12d 2814 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = 𝐵 ↔ (𝐹‘𝐴) = 𝐶)) |
14 | 11, 13 | imbi12d 348 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹‘𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶))) |
15 | 4 | fvmpt2 6756 | . . . 4 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V) → (𝐹‘𝑥) = 𝐵) |
16 | 15 | ex 416 | . . 3 ⊢ (𝑥 ∈ 𝐷 → (𝐵 ∈ V → (𝐹‘𝑥) = 𝐵)) |
17 | 1, 9, 14, 16 | vtoclgaf 3521 | . 2 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)) |
18 | elex 3459 | . 2 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) | |
19 | 17, 18 | impel 509 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 Ⅎwnfc 2936 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-pow 5231 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-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 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-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fv 6332 |
This theorem is referenced by: fvmptnf 6767 elfvmptrab1w 6771 elfvmptrab1 6772 elovmpt3rab1 7385 rdgsucmptf 8047 frsucmpt 8056 fprodntriv 15288 prodss 15293 fprodefsum 15440 dvfsumabs 24626 dvfsumlem1 24629 dvfsumlem4 24632 dvfsum2 24637 dchrisumlem2 26074 dchrisumlem3 26075 rmfsupp2 30917 ptrest 35056 hlhilset 39230 fsumsermpt 42221 mulc1cncfg 42231 expcnfg 42233 climsubmpt 42302 climeldmeqmpt 42310 climfveqmpt 42313 fnlimfvre 42316 climfveqmpt3 42324 climeldmeqmpt3 42331 climinf2mpt 42356 climinfmpt 42357 stoweidlem23 42665 stoweidlem34 42676 stoweidlem36 42678 wallispilem5 42711 stirlinglem4 42719 stirlinglem11 42726 stirlinglem12 42727 stirlinglem13 42728 stirlinglem14 42729 sge0lempt 43049 sge0isummpt2 43071 meadjiun 43105 hoimbl2 43304 vonhoire 43311 |
Copyright terms: Public domain | W3C validator |