Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funbrfv | Structured version Visualization version Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funrel 5905 | . . . 4 | |
2 | brrelex2 5157 | . . . 4 | |
3 | 1, 2 | sylan 488 | . . 3 |
4 | breq2 4657 | . . . . . 6 | |
5 | 4 | anbi2d 740 | . . . . 5 |
6 | eqeq2 2633 | . . . . 5 | |
7 | 5, 6 | imbi12d 334 | . . . 4 |
8 | funeu 5913 | . . . . . 6 | |
9 | tz6.12-1 6210 | . . . . . 6 | |
10 | 8, 9 | sylan2 491 | . . . . 5 |
11 | 10 | anabss7 862 | . . . 4 |
12 | 7, 11 | vtoclg 3266 | . . 3 |
13 | 3, 12 | mpcom 38 | . 2 |
14 | 13 | ex 450 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wceq 1483 wcel 1990 weu 2470 cvv 3200 class class class wbr 4653 wrel 5119 wfun 5882 cfv 5888 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-iota 5851 df-fun 5890 df-fv 5896 |
This theorem is referenced by: funopfv 6235 fnbrfvb 6236 fvelima 6248 fvi 6255 opabiota 6261 fmptco 6396 fliftfun 6562 fliftval 6566 tfrlem5 7476 fpwwe2 9465 nqerid 9755 sum0 14452 sumz 14453 fsumsers 14459 isumclim 14488 ntrivcvgfvn0 14631 ntrivcvgtail 14632 zprodn0 14669 iprodclim 14729 idinv 16449 cnextfvval 21869 cnextfres 21873 dvadd 23703 dvmul 23704 dvco 23710 dvcj 23713 dvrec 23718 dvcnv 23740 dvef 23743 ftc1cn 23806 ulmdv 24157 minvecolem4b 27734 minvecolem4 27736 hlimuni 28095 chscllem4 28499 fmptcof2 29457 fvtransport 32139 fvray 32248 fvline 32251 ftc1cnnc 33484 frege124d 38053 fvelimad 39458 fvelima2 39475 |
Copyright terms: Public domain | W3C validator |