Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fneq2i | Structured version Visualization version Unicode version |
Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.) |
Ref | Expression |
---|---|
fneq2i.1 |
Ref | Expression |
---|---|
fneq2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fneq2i.1 | . 2 | |
2 | fneq2 5980 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wceq 1483 wfn 5883 |
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-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-fn 5891 |
This theorem is referenced by: fnunsn 5998 fnprb 6472 fntpb 6473 fnsuppeq0 7323 tpos0 7382 wfrlem5 7419 dfixp 7910 ordtypelem4 8426 ser0f 12854 0csh0 13539 s3fn 13656 prodf1f 14624 efcvgfsum 14816 prmrec 15626 xpscfn 16219 0ssc 16497 0subcat 16498 mulgfvi 17545 ovolunlem1 23265 volsup 23324 mtest 24158 mtestbdd 24159 pserulm 24176 pserdvlem2 24182 emcllem5 24726 lgamgulm2 24762 lgamcvglem 24766 gamcvg2lem 24785 tglnfn 25442 crctcshlem4 26712 resf1o 29505 esumfsup 30132 esumpcvgval 30140 esumcvg 30148 esumsup 30151 bnj149 30945 bnj1312 31126 faclimlem1 31629 frrlem5 31784 fullfunfnv 32053 knoppcnlem8 32490 knoppcnlem11 32493 mblfinlem2 33447 ovoliunnfl 33451 voliunnfl 33453 subsaliuncl 40576 |
Copyright terms: Public domain | W3C validator |