![]() |
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 7013 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 2919 | . . . 4 ⊢ Ⅎ𝑥 𝐶 ∈ V |
4 | fvmptf.4 | . . . . . . 7 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
5 | nfmpt1 5255 | . . . . . . 7 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐷 ↦ 𝐵) | |
6 | 4, 5 | nfcxfr 2900 | . . . . . 6 ⊢ Ⅎ𝑥𝐹 |
7 | 6, 1 | nffv 6916 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝐴) |
8 | 7, 2 | nfeq 2916 | . . . 4 ⊢ Ⅎ𝑥(𝐹‘𝐴) = 𝐶 |
9 | 3, 8 | nfim 1893 | . . 3 ⊢ Ⅎ𝑥(𝐶 ∈ V → (𝐹‘𝐴) = 𝐶) |
10 | fvmptf.3 | . . . . 5 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
11 | 10 | eleq1d 2823 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V)) |
12 | fveq2 6906 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | |
13 | 12, 10 | eqeq12d 2750 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = 𝐵 ↔ (𝐹‘𝐴) = 𝐶)) |
14 | 11, 13 | imbi12d 344 | . . 3 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹‘𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶))) |
15 | 4 | fvmpt2 7026 | . . . 4 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V) → (𝐹‘𝑥) = 𝐵) |
16 | 15 | ex 412 | . . 3 ⊢ (𝑥 ∈ 𝐷 → (𝐵 ∈ V → (𝐹‘𝑥) = 𝐵)) |
17 | 1, 9, 14, 16 | vtoclgaf 3575 | . 2 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)) |
18 | elex 3498 | . 2 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) | |
19 | 17, 18 | impel 505 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 ∈ wcel 2105 Ⅎwnfc 2887 Vcvv 3477 ↦ cmpt 5230 ‘cfv 6562 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ral 3059 df-rex 3068 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5582 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-iota 6515 df-fun 6564 df-fv 6570 |
This theorem is referenced by: fvmptnf 7037 elfvmptrab1w 7042 elfvmptrab1 7043 elovmpt3rab1 7692 rdgsucmptf 8466 frsucmpt 8476 fprodntriv 15974 prodss 15979 fprodefsum 16127 dvfsumabs 26077 dvfsumlem1 26080 dvfsumlem4 26084 dvfsum2 26089 dchrisumlem2 27548 dchrisumlem3 27549 rmfsupp2 33227 ptrest 37605 hlhilset 41916 fsumsermpt 45534 mulc1cncfg 45544 expcnfg 45546 climsubmpt 45615 climeldmeqmpt 45623 climfveqmpt 45626 fnlimfvre 45629 climfveqmpt3 45637 climeldmeqmpt3 45644 climinf2mpt 45669 climinfmpt 45670 stoweidlem23 45978 stoweidlem34 45989 stoweidlem36 45991 wallispilem5 46024 stirlinglem4 46032 stirlinglem11 46039 stirlinglem12 46040 stirlinglem13 46041 stirlinglem14 46042 sge0lempt 46365 sge0isummpt2 46387 meadjiun 46421 hoimbl2 46620 vonhoire 46627 |
Copyright terms: Public domain | W3C validator |