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 2751 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfeq 2762 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 Ⅎwnf 1699 Ⅎwnfc 2738 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-cleq 2603 df-nfc 2740 |
This theorem is referenced by: euabsn 4205 invdisjrab 4572 disjxun 4581 iunopeqop 4906 opabiotafun 6169 fvmptt 6208 eusvobj2 6542 oprabv 6601 ovmpt2dv2 6692 ov3 6695 dom2lem 7881 pwfseqlem2 9360 fsumf1o 14301 isummulc2 14335 fsum00 14371 isumshft 14410 zprod 14506 fprodf1o 14515 prodss 14516 iserodd 15378 yonedalem4b 16739 gsum2d2lem 18195 gsummptnn0fz 18205 gsummoncoe1 19495 elptr2 21187 ovoliunnul 23082 mbfinf 23238 itg2splitlem 23321 dgrle 23803 disjabrex 28777 disjabrexf 28778 disjunsn 28789 voliune 29619 volfiniune 29620 bnj958 30264 bnj1491 30379 finminlem 31482 poimirlem23 32602 poimirlem28 32607 cdleme43fsv1snlem 34726 ltrniotaval 34887 cdlemksv2 35153 cdlemkuv2 35173 cdlemk36 35219 cdlemkid 35242 cdlemk19x 35249 eq0rabdioph 36358 monotoddzz 36526 cncfiooicclem1 38779 stoweidlem28 38921 stoweidlem48 38941 stoweidlem58 38951 etransclem32 39159 sge0gtfsumgt 39336 voliunsge0lem 39365 |
Copyright terms: Public domain | W3C validator |