![]() |
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 2948 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfeq 2959 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 Ⅎwnf 1766 Ⅎwnfc 2932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1763 df-nf 1767 df-cleq 2787 df-nfc 2934 |
This theorem is referenced by: euabsn 4571 invdisjrab 4951 disjxun 4962 iunopeqop 5305 fvelimad 6603 opabiotafun 6614 fvmptt 6657 eusvobj2 7012 oprabv 7076 ovmpodv2 7167 ov3 7170 dom2lem 8400 pwfseqlem2 9930 fsumf1o 14913 isummulc2 14950 fsum00 14986 isumshft 15027 zprod 15124 fprodf1o 15133 prodss 15134 fprodle 15183 iserodd 16001 yonedalem4b 17355 gsum2d2lem 18813 gsummptnn0fz 18823 gsummoncoe1 20155 elptr2 21866 ovoliunnul 23791 mbfinf 23949 itg2splitlem 24032 dgrle 24516 disjabrex 30014 disjabrexf 30015 disjunsn 30026 voliune 31097 volfiniune 31098 bnj958 31820 bnj1491 31935 finminlem 33269 poimirlem23 34459 poimirlem28 34464 cdleme43fsv1snlem 37100 ltrniotaval 37261 cdlemksv2 37527 cdlemkuv2 37547 cdlemk36 37593 cdlemkid 37616 cdlemk19x 37623 eq0rabdioph 38871 monotoddzz 39038 stoweidlem28 41869 stoweidlem48 41889 stoweidlem58 41899 etransclem32 42107 sge0gtfsumgt 42281 voliunsge0lem 42310 |
Copyright terms: Public domain | W3C validator |