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  5897  elabrexg  5898  nfmpo  6089  cbvmpox  6098  ovmpodxf  6146  fmpox  6364  f1od2  6399  nfrecs  6472  erovlem  6795  xpf1o  7029  mapxpen  7033  mkvprop  7356  cc3  7486  lble  9126  nfsum1  11916  nfsum  11917  zsumdc  11944  fsum3  11947  fsum3cvg2  11954  fsum2dlemstep  11994  mertenslem2  12096  nfcprod1  12114  nfcprod  12115  zproddc  12139  fprod2dlemstep  12182  ctiunctlemfo  13059  ellimc3apf  15383