Theorem nfeq2 2386

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 2374	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2382	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1397  Ⅎwnf 1508  Ⅎwnfc 2361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363

This theorem is referenced by:  issetf  2810  eqvincf  2931  csbhypf  3166  nfpr  3719  intab  3957  nfmpt  4181  cbvmptf  4183  cbvmpt  4184  repizf2  4252  moop2  4344  eusvnf  4550  elrnmpt1  4983  iotaexab  5305  fmptco  5813  elabrex  5898  elabrexg  5899  nfmpo  6090  cbvmpox  6099  ovmpodxf  6147  fmpox  6365  f1od2  6400  nfrecs  6473  erovlem  6796  xpf1o  7030  mapxpen  7034  mkvprop  7357  cc3  7487  lble  9127  nfsum1  11934  nfsum  11935  zsumdc  11963  fsum3  11966  fsum3cvg2  11973  fsum2dlemstep  12013  mertenslem2  12115  nfcprod1  12133  nfcprod  12134  zproddc  12158  fprod2dlemstep  12201  ctiunctlemfo  13078  ellimc3apf  15403