![]() |
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 6504 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 | elex 3399 | . . 3 ⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) | |
2 | fvmptf.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | fvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑥𝐶 | |
4 | 3 | nfel1 2955 | . . . . 5 ⊢ Ⅎ𝑥 𝐶 ∈ V |
5 | fvmptf.4 | . . . . . . . 8 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
6 | nfmpt1 4939 | . . . . . . . 8 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐷 ↦ 𝐵) | |
7 | 5, 6 | nfcxfr 2938 | . . . . . . 7 ⊢ Ⅎ𝑥𝐹 |
8 | 7, 2 | nffv 6420 | . . . . . 6 ⊢ Ⅎ𝑥(𝐹‘𝐴) |
9 | 8, 3 | nfeq 2952 | . . . . 5 ⊢ Ⅎ𝑥(𝐹‘𝐴) = 𝐶 |
10 | 4, 9 | nfim 1996 | . . . 4 ⊢ Ⅎ𝑥(𝐶 ∈ V → (𝐹‘𝐴) = 𝐶) |
11 | fvmptf.3 | . . . . . 6 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
12 | 11 | eleq1d 2862 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V ↔ 𝐶 ∈ V)) |
13 | fveq2 6410 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) | |
14 | 13, 11 | eqeq12d 2813 | . . . . 5 ⊢ (𝑥 = 𝐴 → ((𝐹‘𝑥) = 𝐵 ↔ (𝐹‘𝐴) = 𝐶)) |
15 | 12, 14 | imbi12d 336 | . . . 4 ⊢ (𝑥 = 𝐴 → ((𝐵 ∈ V → (𝐹‘𝑥) = 𝐵) ↔ (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶))) |
16 | 5 | fvmpt2 6515 | . . . . 5 ⊢ ((𝑥 ∈ 𝐷 ∧ 𝐵 ∈ V) → (𝐹‘𝑥) = 𝐵) |
17 | 16 | ex 402 | . . . 4 ⊢ (𝑥 ∈ 𝐷 → (𝐵 ∈ V → (𝐹‘𝑥) = 𝐵)) |
18 | 2, 10, 15, 17 | vtoclgaf 3458 | . . 3 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ V → (𝐹‘𝐴) = 𝐶)) |
19 | 1, 18 | syl5 34 | . 2 ⊢ (𝐴 ∈ 𝐷 → (𝐶 ∈ 𝑉 → (𝐹‘𝐴) = 𝐶)) |
20 | 19 | imp 396 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 Ⅎwnfc 2927 Vcvv 3384 ↦ cmpt 4921 ‘cfv 6100 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 ax-sep 4974 ax-nul 4982 ax-pow 5034 ax-pr 5096 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3386 df-sbc 3633 df-csb 3728 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-sn 4368 df-pr 4370 df-op 4374 df-uni 4628 df-br 4843 df-opab 4905 df-mpt 4922 df-id 5219 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-iota 6063 df-fun 6102 df-fv 6108 |
This theorem is referenced by: fvmptnf 6526 elfvmptrab1 6529 elovmpt3rab1 7126 rdgsucmptf 7762 frsucmpt 7771 fprodntriv 15006 prodss 15011 fprodefsum 15158 dvfsumabs 24124 dvfsumlem1 24127 dvfsumlem4 24130 dvfsum2 24135 dchrisumlem2 25528 dchrisumlem3 25529 ptrest 33890 hlhilset 37948 fvmptd3 40184 fsumsermpt 40544 mulc1cncfg 40554 expcnfg 40556 climsubmpt 40625 climeldmeqmpt 40633 climfveqmpt 40636 fnlimfvre 40639 fnlimfvre2 40642 climfveqmpt3 40647 climeldmeqmpt3 40654 climinf2mpt 40679 climinfmpt 40680 stoweidlem23 40972 stoweidlem34 40983 stoweidlem36 40985 wallispilem5 41018 stirlinglem4 41026 stirlinglem11 41033 stirlinglem12 41034 stirlinglem13 41035 stirlinglem14 41036 sge0lempt 41359 sge0isummpt2 41381 meadjiun 41415 hoimbl2 41614 vonhoire 41621 |
Copyright terms: Public domain | W3C validator |