Theorem nfeq2 2386

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 2374	. 2 |- F/_ x A
2		nfeq2.1	. 2 |- F/_ x B
3	1, 2	nfeq 2382	1 |- F/ x A = B

Syntax hints:   = wceq 1397   F/wnf 1508   F/_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  11921  nfsum  11922  zsumdc  11950  fsum3  11953  fsum3cvg2  11960  fsum2dlemstep  12000  mertenslem2  12102  nfcprod1  12120  nfcprod  12121  zproddc  12145  fprod2dlemstep  12188  ctiunctlemfo  13065  ellimc3apf  15390