Theorem nfeq 2226

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 2075	. 2 |- ( A = B <-> A. z ( z e. A <-> z e. B ) )
2		nfnfc.1	. . . . 5 |- F/_ x A
3	2	nfcri 2213	. . . 4 |- F/ x z e. A
4		nfeq.2	. . . . 5 |- F/_ x B
5	4	nfcri 2213	. . . 4 |- F/ x z e. B
6	3, 5	nfbi 1521	. . 3 |- F/ x ( z e. A <-> z e. B )
7	6	nfal 1508	. 2 |- F/ x A. z ( z e. A <-> z e. B )
8	1, 7	nfxfr 1403	1 |- F/ x A = B

Syntax hints:   <-> wb 103   A.wal 1282   = wceq 1284   F/wnf 1389   e. wcel 1433   F/_wnfc 2206

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-cleq 2074  df-clel 2077  df-nfc 2208

This theorem is referenced by:  nfel  2227  nfeq1  2228  nfeq2  2230  nfne  2337  raleqf  2545  rexeqf  2546  reueq1f  2547  rmoeq1f  2548  rabeqf  2594  sbceqg  2922  csbhypf  2941  nfiotadxy  4890  nffn  5015  nffo  5125  fvmptdf  5279  mpteqb  5282  fvmptf  5284  eqfnfv2f  5290  dff13f  5430  ovmpt2s  5644  ov2gf  5645  ovmpt2dxf  5646  ovmpt2df  5652  eqerlem  6160