![]() |
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 2891 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | 1, 2 | nfeq 2905 | 1 ⊢ Ⅎ𝑥 𝐴 = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 Ⅎwnf 1777 Ⅎwnfc 2875 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-tru 1536 df-ex 1774 df-nf 1778 df-cleq 2717 df-nfc 2877 |
This theorem is referenced by: euabsn 4732 invdisjrabw 5134 invdisjrab 5135 disjxun 5147 iunopeqop 5523 fvelimad 6965 opabiotafun 6978 fvmptt 7024 eusvobj2 7411 oprabv 7480 ovmpodv2 7579 ov3 7584 dom2lem 9013 ttrcltr 9741 pwfseqlem2 10684 fsumf1o 15705 isummulc2 15744 fsum00 15780 isumshft 15821 zprod 15917 fprodf1o 15926 prodss 15927 fprodle 15976 iserodd 16807 yonedalem4b 18271 gsum2d2lem 19940 gsummptnn0fz 19953 gsummoncoe1 22252 elptr2 23522 ovoliunnul 25480 mbfinf 25638 itg2splitlem 25722 dgrle 26222 noinfbnd1 27708 disjabrex 32451 disjabrexf 32452 disjunsn 32463 voliune 33979 volfiniune 33980 bnj958 34702 bnj1491 34819 finminlem 35933 poimirlem23 37247 poimirlem28 37252 cdleme43fsv1snlem 40023 ltrniotaval 40184 cdlemksv2 40450 cdlemkuv2 40470 cdlemk36 40516 cdlemkid 40539 cdlemk19x 40546 eq0rabdioph 42338 monotoddzz 42506 disjinfi 44704 stoweidlem28 45554 stoweidlem48 45574 stoweidlem58 45584 etransclem32 45792 sge0gtfsumgt 45969 voliunsge0lem 45998 |
Copyright terms: Public domain | W3C validator |