Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfne | Structured version Visualization version Unicode version |
Description: Bound-variable hypothesis builder for inequality. (Contributed by NM, 10-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfne.1 | |
nfne.2 |
Ref | Expression |
---|---|
nfne |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2795 | . 2 | |
2 | nfne.1 | . . . 4 | |
3 | nfne.2 | . . . 4 | |
4 | 2, 3 | nfeq 2776 | . . 3 |
5 | 4 | nfn 1784 | . 2 |
6 | 1, 5 | nfxfr 1779 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wceq 1483 wnf 1708 wnfc 2751 wne 2794 |
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-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-cleq 2615 df-nfc 2753 df-ne 2795 |
This theorem is referenced by: cantnflem1 8586 ac6c4 9303 fproddiv 14691 fprodn0 14709 fproddivf 14718 mreiincl 16256 lss1d 18963 iunconn 21231 restmetu 22375 coeeq2 23998 bnj1534 30923 bnj1542 30927 bnj1398 31102 bnj1445 31112 bnj1449 31116 bnj1312 31126 bnj1525 31137 cvmcov 31245 nfwlim 31768 sltval2 31809 finminlem 32312 finxpreclem2 33227 poimirlem25 33434 poimirlem26 33435 poimirlem28 33437 cdleme40m 35755 cdleme40n 35756 dihglblem5 36587 iunconnlem2 39171 eliuniin2 39303 suprnmpt 39355 disjf1 39369 disjrnmpt2 39375 disjinfi 39380 allbutfiinf 39647 fsumiunss 39807 idlimc 39858 0ellimcdiv 39881 stoweidlem31 40248 stoweidlem58 40275 fourierdlem31 40355 sge0iunmpt 40635 |
Copyright terms: Public domain | W3C validator |