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	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	nfbii	⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		nfbii.1	⊢ ( 𝜑 ↔ 𝜓 )
2		nfbiit	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 ) )
3	2 1	mpg	⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 )