Theorem nfeq 2382

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfnfc.1	|- F/_ x A
nfeq.2	|- F/_ x B

Assertion

Ref	Expression
nfeq	|- F/ x A = B

Proof of Theorem nfeq

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2225	. 2 |- ( A = B <-> A. z ( z e. A <-> z e. B ) )
2		nfnfc.1	. . . . 5 |- F/_ x A
3	2	nfcri 2368	. . . 4 |- F/ x z e. A
4		nfeq.2	. . . . 5 |- F/_ x B
5	4	nfcri 2368	. . . 4 |- F/ x z e. B
6	3, 5	nfbi 1637	. . 3 |- F/ x ( z e. A <-> z e. B )
7	6	nfal 1624	. 2 |- F/ x A. z ( z e. A <-> z e. B )
8	1, 7	nfxfr 1522	1 |- F/ x A = B

Syntax hints:   <-> wb 105   A.wal 1395   = wceq 1397   F/wnf 1508   e. wcel 2202   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:  nfel  2383  nfeq1  2384  nfeq2  2386  nfne  2495  raleqf  2726  rexeqf  2727  reueq1f  2728  rmoeq1f  2729  rabeqf  2792  sbceqg  3143  csbhypf  3166  nfiotadw  5289  nffn  5426  nffo  5558  fvmptdf  5734  mpteqb  5737  fvmptf  5739  eqfnfv2f  5748  dff13f  5911  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  ovmpodf  6153  eqerlem  6733  sumeq2  11937  fsumadd  11985  prodeq1f  12131  prodeq2  12136  txcnp  15014  cnmpt11  15026  cnmpt21  15034  cnmptcom  15041  dvmptfsum  15468  lgseisenlem2  15819