Theorem nfeq 2347

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 2190	. 2 |- ( A = B <-> A. z ( z e. A <-> z e. B ) )
2		nfnfc.1	. . . . 5 |- F/_ x A
3	2	nfcri 2333	. . . 4 |- F/ x z e. A
4		nfeq.2	. . . . 5 |- F/_ x B
5	4	nfcri 2333	. . . 4 |- F/ x z e. B
6	3, 5	nfbi 1603	. . 3 |- F/ x ( z e. A <-> z e. B )
7	6	nfal 1590	. 2 |- F/ x A. z ( z e. A <-> z e. B )
8	1, 7	nfxfr 1488	1 |- F/ x A = B

Syntax hints:   <-> wb 105   A.wal 1362   = wceq 1364   F/wnf 1474   e. wcel 2167   F/_wnfc 2326

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  nfel  2348  nfeq1  2349  nfeq2  2351  nfne  2460  raleqf  2689  rexeqf  2690  reueq1f  2691  rmoeq1f  2692  rabeqf  2753  sbceqg  3100  csbhypf  3123  nfiotadw  5222  nffn  5354  nffo  5479  fvmptdf  5649  mpteqb  5652  fvmptf  5654  eqfnfv2f  5663  dff13f  5817  ovmpos  6046  ov2gf  6047  ovmpodxf  6048  ovmpodf  6054  eqerlem  6623  sumeq2  11524  fsumadd  11571  prodeq1f  11717  prodeq2  11722  txcnp  14507  cnmpt11  14519  cnmpt21  14527  cnmptcom  14534  dvmptfsum  14961  lgseisenlem2  15312