Theorem nfeq2 2324

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

Syntax hints:   = wceq 1348   F/wnf 1453   F/_wnfc 2299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301

This theorem is referenced by:  issetf  2737  eqvincf  2855  csbhypf  3087  nfpr  3633  intab  3860  nfmpt  4081  cbvmptf  4083  cbvmpt  4084  repizf2  4148  moop2  4236  eusvnf  4438  elrnmpt1  4862  fmptco  5662  elabrex  5737  nfmpo  5922  cbvmpox  5931  ovmpodxf  5978  fmpox  6179  f1od2  6214  nfrecs  6286  erovlem  6605  xpf1o  6822  mapxpen  6826  mkvprop  7134  cc3  7230  lble  8863  nfsum1  11319  nfsum  11320  zsumdc  11347  fsum3  11350  fsum3cvg2  11357  fsum2dlemstep  11397  mertenslem2  11499  nfcprod1  11517  nfcprod  11518  zproddc  11542  fprod2dlemstep  11585  ctiunctlemfo  12394  ellimc3apf  13423