Theorem nfeq2 2311

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq2.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq2	⊢ Ⅎ𝑥 𝐴 = 𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2

Step	Hyp	Ref	Expression
1		nfcv 2299	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2307	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1335  Ⅎwnf 1440  Ⅎwnfc 2286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-cleq 2150  df-clel 2153  df-nfc 2288

This theorem is referenced by:  issetf  2719  eqvincf  2837  csbhypf  3069  nfpr  3609  intab  3836  nfmpt  4056  cbvmptf  4058  cbvmpt  4059  repizf2  4123  moop2  4211  eusvnf  4413  elrnmpt1  4837  fmptco  5633  elabrex  5708  nfmpo  5890  cbvmpox  5899  ovmpodxf  5946  fmpox  6148  f1od2  6182  nfrecs  6254  erovlem  6572  xpf1o  6789  mapxpen  6793  mkvprop  7101  cc3  7188  lble  8818  nfsum1  11253  nfsum  11254  zsumdc  11281  fsum3  11284  fsum3cvg2  11291  fsum2dlemstep  11331  mertenslem2  11433  nfcprod1  11451  nfcprod  11452  zproddc  11476  fprod2dlemstep  11519  ctiunctlemfo  12168  ellimc3apf  13029