Theorem sbnf

Description: Move nonfree predicate in and out of substitution; see sbal and sbex . (Contributed by BJ, 2-May-2019) (Proof shortened by Wolf Lammen, 2-May-2025)

	Ref	Expression
Assertion	sbnf	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-nf	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
2	1	sbbii	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) )
3		sbim	⊢ ( [ 𝑧 / 𝑦 ] ( ∃ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 → [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
4		sbex	⊢ ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 ↔ ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
5		sbal	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
6	4 5	imbi12i	⊢ ( ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 → [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
7		df-nf	⊢ ( Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ( ∃ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
8	6 7	bitr4i	⊢ ( ( [ 𝑧 / 𝑦 ] ∃ 𝑥 𝜑 → [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
9	2 3 8	3bitri	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )