Theorem nfbii

Description: Equality theorem for the non-freeness predicate. (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)

	Ref	Expression
Hypothesis	nfbii.1	$$⊢\phi \leftrightarrow \psi$$
Assertion	nfbii	$$⊢Ⅎx\phi \leftrightarrow Ⅎx\psi$$

Proof

Step	Hyp	Ref	Expression
1		nfbii.1	$$⊢\phi \leftrightarrow \psi$$
2		nfbiit	$$⊢\forall x\left(\phi \leftrightarrow \psi \right)\to \left(Ⅎx\phi \leftrightarrow Ⅎx\psi \right)$$
3	2 1	mpg	$$⊢Ⅎx\phi \leftrightarrow Ⅎx\psi$$