![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfne | Structured version Visualization version GIF 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 2941 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | nfne.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfne.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | 2, 3 | nfeq 2917 | . . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
5 | 4 | nfn 1861 | . 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵 |
6 | 1, 5 | nfxfr 1856 | 1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1542 Ⅎwnf 1786 Ⅎwnfc 2884 ≠ wne 2940 |
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-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-cleq 2725 df-nfc 2886 df-ne 2941 |
This theorem is referenced by: cantnflem1 9630 ac6c4 10422 fproddiv 15849 fprodn0 15867 fproddivf 15875 mreiincl 17481 lss1d 20439 iunconn 22795 restmetu 23942 coeeq2 25619 sltval2 27020 fedgmullem2 32382 bnj1534 33522 bnj1542 33526 bnj1398 33703 bnj1445 33713 bnj1449 33717 bnj1312 33727 bnj1525 33738 cvmcov 33914 nfwlim 34453 finminlem 34836 finxpreclem2 35907 poimirlem25 36149 poimirlem26 36150 poimirlem28 36152 cdleme40m 38976 cdleme40n 38977 dihglblem5 39807 iunconnlem2 43305 eliuniin2 43418 disjf1 43489 disjrnmpt2 43495 disjinfi 43500 allbutfiinf 43741 fsumiunss 43902 idlimc 43953 0ellimcdiv 43976 stoweidlem31 44358 stoweidlem58 44385 fourierdlem31 44465 sge0iunmpt 44745 |
Copyright terms: Public domain | W3C validator |