![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > nfeq | Unicode version |
Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.) |
Ref | Expression |
---|---|
nfnfc.1 | |
nfeq.2 |
Ref | Expression |
---|---|
nfeq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnfc.1 | . . . 4 | |
2 | 1 | a1i 11 | . . 3 |
3 | nfeq.2 | . . . 4 | |
4 | 3 | a1i 11 | . . 3 |
5 | 2, 4 | nfeqd 2626 | . 2 |
6 | 5 | trud 1404 | 1 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1395 wtru 1396 F/ wnf 1616 F/_ wnfc 2605 |
This theorem is referenced by: nfelOLD 2633 nfeq1 2634 nfeq2 2636 nfne 2788 raleqf 3050 rexeqf 3051 reueq1f 3052 rmoeq1f 3053 rabeqf 3102 csbhypf 3453 sbceqg 3825 nffn 5682 nffo 5799 fvmptdf 5967 mpteqb 5970 fvmptf 5972 eqfnfv2f 5985 dff13f 6167 ovmpt2s 6426 ov2gf 6427 ovmpt2dxf 6428 ovmpt2df 6434 eqerlem 7362 seqof2 12165 sumeq2ii 13515 sumss 13546 fsumadd 13561 fsummulc2 13599 fsumrelem 13621 prodeq1f 13715 prodeq2ii 13720 fprodmul 13765 fproddiv 13766 txcnp 20121 ptcnplem 20122 cnmpt11 20164 cnmpt21 20172 cnmptcom 20179 mbfeqalem 22049 mbflim 22075 itgeq1f 22178 itgeqa 22220 dvmptfsum 22376 ulmss 22792 leibpi 23273 o1cxp 23304 lgseisenlem2 23625 subtr 30132 subtr2 30133 iuneq2f 30563 mpt2bi123f 30571 mptbi12f 30575 dvdsrabdioph 30743 fphpd 30750 fvelrnbf 31393 refsum2cnlem1 31412 fmuldfeq 31577 fprodle 31604 mccl 31606 climmulf 31610 climexp 31611 climsuse 31614 climrecf 31615 climaddf 31621 mullimc 31622 neglimc 31653 addlimc 31654 0ellimcdiv 31655 dvnmptdivc 31735 dvmptfprod 31742 dvnprodlem1 31743 stoweidlem18 31800 stoweidlem31 31813 stoweidlem55 31837 stoweidlem59 31841 ovmpt2rdxf 32928 bnj1316 33879 bnj1446 34101 bnj1447 34102 bnj1448 34103 bnj1519 34121 bnj1520 34122 bnj1529 34126 bj-sbeqALT 34467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-10 1837 ax-11 1842 ax-12 1854 ax-ext 2435 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1398 df-ex 1613 df-nf 1617 df-cleq 2449 df-nfc 2607 |
Copyright terms: Public domain | W3C validator |