Theorem nfeq 2496

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 2483	. . . 4 |- F/x z e. A
4		nfeq.2	. . . . 5 |- F/_xB
5	4	nfcri 2483	. . . 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 2476

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 2478

This theorem is referenced by:  nfel  2497  nfeq1  2498  nfeq2  2500  nfne  2610  raleqf  2803  rexeqf  2804  reueq1f  2805  rmoeq1f  2806  rabeqf  2852  sbceqg  3152  csbhypf  3171  nffn  5180  nffo  5268  eqfnfv2f  5396  dff13f  5472  ov2gf  5711  fvmptf  5722