Theorem nfeq2 2230

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

Hypothesis

Ref	Expression
nfeq2.1	|- F/_ x B

Assertion

Ref	Expression
nfeq2	|- F/ x A = B

Distinct variable group:   x, A

Allowed substitution hint:   B( x)

Proof of Theorem nfeq2

Step	Hyp	Ref	Expression
1		nfcv 2219	. 2 |- F/_ x A
2		nfeq2.1	. 2 |- F/_ x B
3	1, 2	nfeq 2226	1 |- F/ x A = B

Syntax hints:   = wceq 1284   F/wnf 1389   F/_wnfc 2206

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-cleq 2074  df-clel 2077  df-nfc 2208

This theorem is referenced by:  issetf  2606  eqvincf  2720  csbhypf  2941  nfpr  3442  intab  3665  nfmpt  3870  cbvmpt  3872  repizf2  3936  moop2  4006  eusvnf  4203  elrnmpt1  4603  fmptco  5351  elabrex  5418  nfmpt2  5593  cbvmpt2x  5602  ovmpt2dxf  5646  fmpt2x  5846  f1od2  5876  nfrecs  5945  erovlem  6221  lble  8025  nfsum1  10193  nfsum  10194