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 3014 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | nfne.1 | . . . 4 ⊢ Ⅎ𝑥𝐴 | |
3 | nfne.2 | . . . 4 ⊢ Ⅎ𝑥𝐵 | |
4 | 2, 3 | nfeq 2988 | . . 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 2958 ≠ wne 3013 |
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 2790 |
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 2811 df-nfc 2960 df-ne 3014 |
This theorem is referenced by: cantnflem1 9140 ac6c4 9891 fproddiv 15303 fprodn0 15321 fproddivf 15329 mreiincl 16855 lss1d 19664 iunconn 21964 restmetu 23107 coeeq2 24759 fedgmullem2 30925 bnj1534 32024 bnj1542 32028 bnj1398 32203 bnj1445 32213 bnj1449 32217 bnj1312 32227 bnj1525 32238 cvmcov 32407 nfwlim 33006 sltval2 33060 finminlem 33563 finxpreclem2 34553 poimirlem25 34798 poimirlem26 34799 poimirlem28 34801 cdleme40m 37483 cdleme40n 37484 dihglblem5 38314 iunconnlem2 41146 eliuniin2 41263 suprnmpt 41306 disjf1 41319 disjrnmpt2 41325 disjinfi 41330 allbutfiinf 41570 fsumiunss 41732 idlimc 41783 0ellimcdiv 41806 stoweidlem31 42193 stoweidlem58 42220 fourierdlem31 42300 sge0iunmpt 42577 |
Copyright terms: Public domain | W3C validator |