Theorem nfeq2 2384

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

Syntax hints:   = wceq 1395  Ⅎwnf 1506  Ⅎwnfc 2359

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  issetf  2808  eqvincf  2929  csbhypf  3164  nfpr  3717  intab  3955  nfmpt  4179  cbvmptf  4181  cbvmpt  4182  repizf2  4250  moop2  4342  eusvnf  4548  elrnmpt1  4981  iotaexab  5303  fmptco  5809  elabrex  5893  elabrexg  5894  nfmpo  6085  cbvmpox  6094  ovmpodxf  6142  fmpox  6360  f1od2  6395  nfrecs  6468  erovlem  6791  xpf1o  7025  mapxpen  7029  mkvprop  7348  cc3  7477  lble  9117  nfsum1  11907  nfsum  11908  zsumdc  11935  fsum3  11938  fsum3cvg2  11945  fsum2dlemstep  11985  mertenslem2  12087  nfcprod1  12105  nfcprod  12106  zproddc  12130  fprod2dlemstep  12173  ctiunctlemfo  13050  ellimc3apf  15374