| 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 2919 | . . 3 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
| 5 | 4 | nfn 1857 | . 2 ⊢ Ⅎ𝑥 ¬ 𝐴 = 𝐵 |
| 6 | 1, 5 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥 𝐴 ≠ 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 = wceq 1540 Ⅎwnf 1783 Ⅎwnfc 2890 ≠ wne 2940 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-nfc 2892 df-ne 2941 |
| This theorem is referenced by: cantnflem1 9729 ac6c4 10521 fproddiv 15997 fprodn0 16015 fproddivf 16023 mreiincl 17639 lss1d 20961 iunconn 23436 restmetu 24583 coeeq2 26281 sltval2 27701 fedgmullem2 33681 bnj1534 34867 bnj1542 34871 bnj1398 35048 bnj1445 35058 bnj1449 35062 bnj1312 35072 bnj1525 35083 cvmcov 35268 nfwlim 35823 finminlem 36319 finxpreclem2 37391 poimirlem25 37652 poimirlem26 37653 poimirlem28 37655 cdleme40m 40469 cdleme40n 40470 dihglblem5 41300 iunconnlem2 44955 eliuniin2 45125 disjf1 45188 disjrnmpt2 45193 disjinfi 45197 allbutfiinf 45431 fsumiunss 45590 idlimc 45641 0ellimcdiv 45664 stoweidlem31 46046 stoweidlem58 46073 fourierdlem31 46153 sge0iunmpt 46433 |
| Copyright terms: Public domain | W3C validator |