Theorem nfbiit

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

Proof

Step	Hyp	Ref	Expression
1		exbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∃ 𝑥 𝜑 ↔ ∃ 𝑥 𝜓 ) )
2		albi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 𝜓 ) )
3	1 2	imbi12d	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) ) )
4		df-nf	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
5		df-nf	⊢ ( Ⅎ 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 → ∀ 𝑥 𝜓 ) )
6	3 4 5	3bitr4g	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 ) )