Theorem nfeq2 2360

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

Syntax hints:   = wceq 1373   F/wnf 1483   F/_wnfc 2335

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337

This theorem is referenced by:  issetf  2779  eqvincf  2898  csbhypf  3132  nfpr  3683  intab  3914  nfmpt  4137  cbvmptf  4139  cbvmpt  4140  repizf2  4207  moop2  4297  eusvnf  4501  elrnmpt1  4930  iotaexab  5251  fmptco  5748  elabrex  5828  elabrexg  5829  nfmpo  6016  cbvmpox  6025  ovmpodxf  6073  fmpox  6288  f1od2  6323  nfrecs  6395  erovlem  6716  xpf1o  6943  mapxpen  6947  mkvprop  7262  cc3  7382  lble  9022  nfsum1  11700  nfsum  11701  zsumdc  11728  fsum3  11731  fsum3cvg2  11738  fsum2dlemstep  11778  mertenslem2  11880  nfcprod1  11898  nfcprod  11899  zproddc  11923  fprod2dlemstep  11966  ctiunctlemfo  12843  ellimc3apf  15165