| 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 2905 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 3 | 1, 2 | nfeq 2919 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 Ⅎwnf 1783 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-nfc 2892 |
| This theorem is referenced by: euabsn 4726 invdisjrab 5130 disjxun 5141 iunopeqop 5526 fvelimad 6976 opabiotafun 6989 fvmptt 7036 eusvobj2 7423 oprabv 7493 ovmpodv2 7591 ov3 7596 dom2lem 9032 ttrcltr 9756 pwfseqlem2 10699 fsumf1o 15759 isummulc2 15798 fsum00 15834 isumshft 15875 zprod 15973 fprodf1o 15982 prodss 15983 fprodle 16032 iserodd 16873 yonedalem4b 18321 gsum2d2lem 19991 gsummptnn0fz 20004 gsummoncoe1 22312 elptr2 23582 ovoliunnul 25542 mbfinf 25700 itg2splitlem 25783 dgrle 26282 noinfbnd1 27774 disjabrex 32595 disjabrexf 32596 disjunsn 32607 voliune 34230 volfiniune 34231 bnj958 34954 bnj1491 35071 finminlem 36319 poimirlem23 37650 poimirlem28 37655 cdleme43fsv1snlem 40422 ltrniotaval 40583 cdlemksv2 40849 cdlemkuv2 40869 cdlemk36 40915 cdlemkid 40938 cdlemk19x 40945 eq0rabdioph 42787 monotoddzz 42955 disjinfi 45197 dvnprodlem1 45961 stoweidlem28 46043 stoweidlem48 46063 stoweidlem58 46073 etransclem32 46281 sge0f1o 46397 sge0gtfsumgt 46458 voliunsge0lem 46487 |
| Copyright terms: Public domain | W3C validator |