Theorem nfeq1 2384

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq1.1	|- F/_ x A

Assertion

Ref	Expression
nfeq1	|- F/ x A = B

Distinct variable group:   x, B

Allowed substitution hint:   A( x)

Proof of Theorem nfeq1

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 |- F/_ x A
2		nfcv 2374	. 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:  euabsn  3741  invdisjrab  4082  fvmptt  5738  eusvobj2  6004  ovmpodv2  6155  ovi3  6159  dom2lem  6945  seq3f1olemstep  10777  seq3f1olemp  10778  fsumf1o  11969  isumss  11970  isummulc2  12005  fsum00  12041  isumshft  12069  fprodf1o  12167  prodssdc  12168