Theorem nfeq2 2240

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

Syntax hints:   = wceq 1289   F/wnf 1394   F/_wnfc 2215

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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217

This theorem is referenced by:  issetf  2626  eqvincf  2742  csbhypf  2966  nfpr  3492  intab  3717  nfmpt  3930  cbvmptf  3932  cbvmpt  3933  repizf2  3997  moop2  4078  eusvnf  4275  elrnmpt1  4686  fmptco  5464  elabrex  5537  nfmpt2  5717  cbvmpt2x  5726  ovmpt2dxf  5770  fmpt2x  5970  f1od2  6000  nfrecs  6072  erovlem  6384  xpf1o  6560  mapxpen  6564  lble  8408  nfsum1  10745  nfsum  10746  zisum  10774  fisum  10778  fisumcvg2  10786  fsum3cvg2  10787  fsum2dlemstep  10828  mertenslem2  10930