Theorem nfeq2 2348

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

Syntax hints:   = wceq 1364   F/wnf 1471   F/_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  2886  csbhypf  3120  nfpr  3669  intab  3900  nfmpt  4122  cbvmptf  4124  cbvmpt  4125  repizf2  4192  moop2  4281  eusvnf  4485  elrnmpt1  4914  iotaexab  5234  fmptco  5725  elabrex  5801  elabrexg  5802  nfmpo  5988  cbvmpox  5997  ovmpodxf  6045  fmpox  6255  f1od2  6290  nfrecs  6362  erovlem  6683  xpf1o  6902  mapxpen  6906  mkvprop  7219  cc3  7330  lble  8968  nfsum1  11502  nfsum  11503  zsumdc  11530  fsum3  11533  fsum3cvg2  11540  fsum2dlemstep  11580  mertenslem2  11682  nfcprod1  11700  nfcprod  11701  zproddc  11725  fprod2dlemstep  11768  ctiunctlemfo  12599  ellimc3apf  14839