| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > nfeq1 | Structured version Visualization version GIF 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 2898 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 3 | 1, 2 | nfeq 2912 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1541 Ⅎwnf 1784 Ⅎwnfc 2883 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1544 df-ex 1781 df-nf 1785 df-cleq 2728 df-nfc 2885 |
| This theorem is referenced by: euabsn 4683 invdisjrab 5085 disjxun 5096 iunopeqop 5469 fvelimad 6901 opabiotafun 6914 fvmptt 6961 eusvobj2 7350 oprabv 7418 ovmpodv2 7516 ov3 7521 dom2lem 8929 ttrcltr 9625 pwfseqlem2 10570 fsumf1o 15646 isummulc2 15685 fsum00 15721 isumshft 15762 zprod 15860 fprodf1o 15869 prodss 15870 fprodle 15919 iserodd 16763 yonedalem4b 18199 gsum2d2lem 19902 gsummptnn0fz 19915 gsummoncoe1 22252 elptr2 23518 ovoliunnul 25464 mbfinf 25622 itg2splitlem 25705 dgrle 26204 noinfbnd1 27697 disjabrex 32657 disjabrexf 32658 disjunsn 32669 voliune 34386 volfiniune 34387 bnj958 35096 bnj1491 35213 finminlem 36512 poimirlem23 37844 poimirlem28 37849 cdleme43fsv1snlem 40680 ltrniotaval 40841 cdlemksv2 41107 cdlemkuv2 41127 cdlemk36 41173 cdlemkid 41196 cdlemk19x 41203 eq0rabdioph 43018 monotoddzz 43185 disjinfi 45436 dvnprodlem1 46190 stoweidlem28 46272 stoweidlem48 46292 stoweidlem58 46302 etransclem32 46510 sge0f1o 46626 sge0gtfsumgt 46687 voliunsge0lem 46716 |
| Copyright terms: Public domain | W3C validator |