Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqfnfvd | Structured version Visualization version Unicode version |
Description: Deduction for equality of functions. (Contributed by Mario Carneiro, 24-Jul-2014.) |
Ref | Expression |
---|---|
eqfnfvd.1 | |
eqfnfvd.2 | |
eqfnfvd.3 |
Ref | Expression |
---|---|
eqfnfvd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqfnfvd.3 | . . 3 | |
2 | 1 | ralrimiva 2966 | . 2 |
3 | eqfnfvd.1 | . . 3 | |
4 | eqfnfvd.2 | . . 3 | |
5 | eqfnfv 6311 | . . 3 | |
6 | 3, 4, 5 | syl2anc 693 | . 2 |
7 | 2, 6 | mpbird 247 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wcel 1990 wral 2912 wfn 5883 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-8 1992 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-pow 4843 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-csb 3534 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-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-fv 5896 |
This theorem is referenced by: foeqcnvco 6555 f1eqcocnv 6556 offveq 6918 tfrlem1 7472 ackbij2lem2 9062 ackbij2lem3 9063 fpwwe2lem8 9459 seqfeq2 12824 seqfeq 12826 seqfeq3 12851 ccatlid 13369 ccatrid 13370 ccatass 13371 swrdid 13428 ccatswrd 13456 swrdccat1 13457 swrdccat2 13458 swrdswrd 13460 cats1un 13475 swrdccatin1 13483 swrdccatin2 13487 swrdccatin12 13491 revccat 13515 revrev 13516 cshco 13582 swrdco 13583 seqshft 13825 seq1st 15284 xpsfeq 16224 yonedainv 16921 pwsco1mhm 17370 f1otrspeq 17867 pmtrfinv 17881 symgtrinv 17892 frgpup3lem 18190 ablfac1eu 18472 psrlidm 19403 psrridm 19404 psrass1 19405 subrgascl 19498 evlslem1 19515 psgndiflemB 19946 frlmup1 20137 frlmup3 20139 frlmup4 20140 mavmulass 20355 upxp 21426 uptx 21428 cnextfres1 21872 ovolshftlem1 23277 volsup 23324 dvidlem 23679 dvrec 23718 dveq0 23763 dv11cn 23764 ftc1cn 23806 coemulc 24011 aannenlem1 24083 ulmuni 24146 ulmdv 24157 ostthlem1 25316 nvinvfval 27495 sspn 27591 kbass2 28976 xppreima2 29450 psgnfzto1stlem 29850 indpreima 30087 esumcvg 30148 signstres 30652 hgt750lemb 30734 subfacp1lem4 31165 cvmliftmolem2 31264 msubff1 31453 iprodefisumlem 31626 poimirlem8 33417 poimirlem13 33422 poimirlem14 33423 ftc1cnnc 33484 eqlkr3 34388 cdleme51finvN 35844 ismrcd2 37262 rfovcnvf1od 38298 dssmapntrcls 38426 dvconstbi 38533 fsumsermpt 39811 icccncfext 40100 voliooicof 40213 etransclem35 40486 rrxsnicc 40520 ovolval4lem1 40863 ccatpfx 41409 pfxccat1 41410 pfxccatin12 41425 zrinitorngc 42000 zrtermorngc 42001 zrtermoringc 42070 |
Copyright terms: Public domain | W3C validator |