Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfeq1 | Structured version Visualization version Unicode version |
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
nfeq1.1 |
Ref | Expression |
---|---|
nfeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfeq1.1 | . 2 | |
2 | nfcv 2764 | . 2 | |
3 | 1, 2 | nfeq 2776 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wceq 1483 wnf 1708 wnfc 2751 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-cleq 2615 df-nfc 2753 |
This theorem is referenced by: euabsn 4261 invdisjrab 4639 disjxun 4651 iunopeqop 4981 opabiotafun 6259 fvmptt 6300 eusvobj2 6643 oprabv 6703 ovmpt2dv2 6794 ov3 6797 dom2lem 7995 pwfseqlem2 9481 fsumf1o 14454 isummulc2 14493 fsum00 14530 isumshft 14571 zprod 14667 fprodf1o 14676 prodss 14677 iserodd 15540 yonedalem4b 16916 gsum2d2lem 18372 gsummptnn0fz 18382 gsummoncoe1 19674 elptr2 21377 ovoliunnul 23275 mbfinf 23432 itg2splitlem 23515 dgrle 23999 disjabrex 29395 disjabrexf 29396 disjunsn 29407 voliune 30292 volfiniune 30293 bnj958 31010 bnj1491 31125 finminlem 32312 poimirlem23 33432 poimirlem28 33437 cdleme43fsv1snlem 35708 ltrniotaval 35869 cdlemksv2 36135 cdlemkuv2 36155 cdlemk36 36201 cdlemkid 36224 cdlemk19x 36231 eq0rabdioph 37340 monotoddzz 37508 cncfiooicclem1 40106 stoweidlem28 40245 stoweidlem48 40265 stoweidlem58 40275 etransclem32 40483 sge0gtfsumgt 40660 voliunsge0lem 40689 |
Copyright terms: Public domain | W3C validator |