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 3017 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | nfne.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfne.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | 2, 3 | nfeq 2991 | . . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
5 | 4 | nfn 1848 | . 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵 |
6 | 1, 5 | nfxfr 1844 | 1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 Ⅎwnf 1775 Ⅎwnfc 2961 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-cleq 2814 df-nfc 2963 df-ne 3017 |
This theorem is referenced by: cantnflem1 9141 ac6c4 9892 fproddiv 15305 fprodn0 15323 fproddivf 15331 mreiincl 16857 lss1d 19666 iunconn 21966 restmetu 23109 coeeq2 24761 fedgmullem2 30926 bnj1534 32025 bnj1542 32029 bnj1398 32204 bnj1445 32214 bnj1449 32218 bnj1312 32228 bnj1525 32239 cvmcov 32408 nfwlim 33007 sltval2 33061 finminlem 33564 finxpreclem2 34554 poimirlem25 34799 poimirlem26 34800 poimirlem28 34802 cdleme40m 37485 cdleme40n 37486 dihglblem5 38316 iunconnlem2 41149 eliuniin2 41267 suprnmpt 41310 disjf1 41323 disjrnmpt2 41329 disjinfi 41334 allbutfiinf 41574 fsumiunss 41736 idlimc 41787 0ellimcdiv 41810 stoweidlem31 42197 stoweidlem58 42224 fourierdlem31 42304 sge0iunmpt 42581 |
Copyright terms: Public domain | W3C validator |