Description: Equivalence theorem for the non-freeness predicate. Closed form of nfbii . (Contributed by Giovanni Mascellani, 10-Apr-2018) Reduce axiom usage. (Revised by BJ, 6-May-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | nfbiit |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exbi | ||
2 | albi | ||
3 | 1 2 | imbi12d | |
4 | df-nf | ||
5 | df-nf | ||
6 | 3 4 5 | 3bitr4g |