Theorem bj-sbnf

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

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

Proof

Step	Hyp	Ref	Expression
1		sbim	⊢ ( [ 𝑧 / 𝑦 ] ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
2		sbal	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
3	2	imbi2i	⊢ ( ( [ 𝑧 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) ↔ ( [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
4	1 3	bitri	⊢ ( [ 𝑧 / 𝑦 ] ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ( [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
5	4	albii	⊢ ( ∀ 𝑥 [ 𝑧 / 𝑦 ] ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑥 ( [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
6		nf5	⊢ ( Ⅎ 𝑥 𝜑 ↔ ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
7	6	sbbii	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
8		sbal	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] ( 𝜑 → ∀ 𝑥 𝜑 ) )
9	7 8	bitri	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] ( 𝜑 → ∀ 𝑥 𝜑 ) )
10		nf5	⊢ ( Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ( [ 𝑧 / 𝑦 ] 𝜑 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
11	5 9 10	3bitr4i	⊢ ( [ 𝑧 / 𝑦 ] Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )