![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funbrfv | Structured version Visualization version GIF version |
Description: The second argument of a binary relation on a function is the function's value. (Contributed by NM, 30-Apr-2004.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Ref | Expression |
---|---|
funbrfv | ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funrel 6563 | . . . 4 ⊢ (Fun 𝐹 → Rel 𝐹) | |
2 | brrelex2 5729 | . . . 4 ⊢ ((Rel 𝐹 ∧ 𝐴𝐹𝐵) → 𝐵 ∈ V) | |
3 | 1, 2 | sylan 581 | . . 3 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → 𝐵 ∈ V) |
4 | breq2 5152 | . . . . . 6 ⊢ (𝑦 = 𝐵 → (𝐴𝐹𝑦 ↔ 𝐴𝐹𝐵)) | |
5 | 4 | anbi2d 630 | . . . . 5 ⊢ (𝑦 = 𝐵 → ((Fun 𝐹 ∧ 𝐴𝐹𝑦) ↔ (Fun 𝐹 ∧ 𝐴𝐹𝐵))) |
6 | eqeq2 2745 | . . . . 5 ⊢ (𝑦 = 𝐵 → ((𝐹‘𝐴) = 𝑦 ↔ (𝐹‘𝐴) = 𝐵)) | |
7 | 5, 6 | imbi12d 345 | . . . 4 ⊢ (𝑦 = 𝐵 → (((Fun 𝐹 ∧ 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦) ↔ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵))) |
8 | funeu 6571 | . . . . . 6 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝑦) → ∃!𝑦 𝐴𝐹𝑦) | |
9 | tz6.12-1 6912 | . . . . . 6 ⊢ ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦) | |
10 | 8, 9 | sylan2 594 | . . . . 5 ⊢ ((𝐴𝐹𝑦 ∧ (Fun 𝐹 ∧ 𝐴𝐹𝑦)) → (𝐹‘𝐴) = 𝑦) |
11 | 10 | anabss7 672 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝑦) → (𝐹‘𝐴) = 𝑦) |
12 | 7, 11 | vtoclg 3557 | . . 3 ⊢ (𝐵 ∈ V → ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵)) |
13 | 3, 12 | mpcom 38 | . 2 ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐹‘𝐴) = 𝐵) |
14 | 13 | ex 414 | 1 ⊢ (Fun 𝐹 → (𝐴𝐹𝐵 → (𝐹‘𝐴) = 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃!weu 2563 Vcvv 3475 class class class wbr 5148 Rel wrel 5681 Fun wfun 6535 ‘cfv 6541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-iota 6493 df-fun 6543 df-fv 6549 |
This theorem is referenced by: funopfv 6941 fnbrfvb 6942 fvelima 6955 fvelimad 6957 fvi 6965 opabiota 6972 fmptco 7124 fliftfun 7306 fliftval 7310 tfrlem5 8377 fpwwe2 10635 nqerid 10925 sum0 15664 sumz 15665 fsumsers 15671 isumclim 15700 ntrivcvgfvn0 15842 ntrivcvgtail 15843 zprodn0 15880 iprodclim 15939 idinv 17733 cnextfvval 23561 cnextfres 23565 dvadd 25449 dvmul 25450 dvco 25456 dvcj 25459 dvrec 25464 dvcnv 25486 dvef 25489 ftc1cn 25552 ulmdv 25907 minvecolem4b 30119 minvecolem4 30121 hlimuni 30479 chscllem4 30881 fmptcof2 31870 fvtransport 34993 fvray 35102 fvline 35105 ftc1cnnc 36549 iscard4 42270 frege124d 42498 fvelima2 43951 |
Copyright terms: Public domain | W3C validator |