Theorem nfeq2 2348

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

Syntax hints:   = wceq 1364  Ⅎwnf 1471  Ⅎwnfc 2323

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-cleq 2186  df-clel 2189  df-nfc 2325

This theorem is referenced by:  issetf  2767  eqvincf  2885  csbhypf  3119  nfpr  3668  intab  3899  nfmpt  4121  cbvmptf  4123  cbvmpt  4124  repizf2  4191  moop2  4280  eusvnf  4484  elrnmpt1  4913  iotaexab  5233  fmptco  5724  elabrex  5800  elabrexg  5801  nfmpo  5987  cbvmpox  5996  ovmpodxf  6044  fmpox  6253  f1od2  6288  nfrecs  6360  erovlem  6681  xpf1o  6900  mapxpen  6904  mkvprop  7217  cc3  7328  lble  8966  nfsum1  11499  nfsum  11500  zsumdc  11527  fsum3  11530  fsum3cvg2  11537  fsum2dlemstep  11577  mertenslem2  11679  nfcprod1  11697  nfcprod  11698  zproddc  11722  fprod2dlemstep  11765  ctiunctlemfo  12596  ellimc3apf  14814