Theorem nfeq 2497

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

Hypotheses

Ref	Expression
nfnfc.1	|- F/_xA
nfeq.2	|- F/_xB

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 2347	. 2 |- (A = B <-> A.z(z e. A <-> z e. B))
2		nfnfc.1	. . . . 5 |- F/_xA
3	2	nfcri 2484	. . . 4 |- F/x z e. A
4		nfeq.2	. . . . 5 |- F/_xB
5	4	nfcri 2484	. . . 4 |- F/x z e. B
6	3, 5	nfbi 1834	. . 3 |- F/x(z e. A <-> z e. B)
7	6	nfal 1842	. 2 |- F/xA.z(z e. A <-> z e. B)
8	1, 7	nfxfr 1570	1 |- F/x A = B

Syntax hints:   <-> wb 176  A.wal 1540   F/wnf 1544   = wceq 1642   e. wcel 1710   F/_wnfc 2477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2479

This theorem is referenced by:  nfel  2498  nfeq1  2499  nfeq2  2501  nfne  2611  raleqf  2804  rexeqf  2805  reueq1f  2806  rmoeq1f  2807  rabeqf  2853  sbceqg  3153  csbhypf  3172  nffn  5181  nffo  5269  eqfnfv2f  5397  dff13f  5473  ov2gf  5712  fvmptf  5723