Theorem nfbii 1644

Description: Equality theorem for not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfbii.1

Assertion

Ref	Expression
nfbii

Proof of Theorem nfbii

Step	Hyp	Ref	Expression
1		nfbii.1	. . . 4
2	1	albii 1640	. . . 4
3	1, 2	imbi12i 326	. . 3
4	3	albii 1640	. 2
5		df-nf 1617	. 2
6		df-nf 1617	. 2
7	4, 5, 6	3bitr4i 277	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616

This theorem is referenced by:  nfxfr  1645  nfxfrd  1646  dvelimhw  1955  nfeqf1  2043  nfceqiOLD  2616  dfnfc2  4267  iunconlem2  33735  bj-nfcf  34492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631

This theorem depends on definitions:  df-bi 185  df-nf 1617