![]() |
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 2941 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfeq 2953 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1653 Ⅎwnf 1879 Ⅎwnfc 2928 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2777 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-cleq 2792 df-nfc 2930 |
This theorem is referenced by: euabsn 4450 invdisjrab 4830 disjxun 4841 iunopeqop 5177 opabiotafun 6484 fvmptt 6525 eusvobj2 6871 oprabv 6937 ovmpt2dv2 7028 ov3 7031 dom2lem 8235 pwfseqlem2 9769 fsumf1o 14795 isummulc2 14832 fsum00 14868 isumshft 14909 zprod 15004 fprodf1o 15013 prodss 15014 iserodd 15873 yonedalem4b 17231 gsum2d2lem 18687 gsummptnn0fz 18697 gsummptnn0fzOLD 18698 gsummoncoe1 19996 elptr2 21706 ovoliunnul 23615 mbfinf 23773 itg2splitlem 23856 dgrle 24340 disjabrex 29912 disjabrexf 29913 disjunsn 29924 voliune 30808 volfiniune 30809 bnj958 31527 bnj1491 31642 finminlem 32825 poimirlem23 33921 poimirlem28 33926 cdleme43fsv1snlem 36441 ltrniotaval 36602 cdlemksv2 36868 cdlemkuv2 36888 cdlemk36 36934 cdlemkid 36957 cdlemk19x 36964 eq0rabdioph 38126 monotoddzz 38293 cncfiooicclem1 40850 stoweidlem28 40988 stoweidlem48 41008 stoweidlem58 41018 etransclem32 41226 sge0gtfsumgt 41403 voliunsge0lem 41432 |
Copyright terms: Public domain | W3C validator |