Theorem sbcalf

Description: Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019)

	Ref	Expression
Hypothesis	sbcalf.1	⊢ Ⅎ 𝑦 𝐴
Assertion	sbcalf	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcalf.1	⊢ Ⅎ 𝑦 𝐴
2		sb8v	⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
3	2	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 𝜑 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
4		sbcal	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
5		nfs1v	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
6	1 5	nfsbcw	⊢ Ⅎ 𝑦 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
7		nfv	⊢ Ⅎ 𝑧 [ 𝐴 / 𝑥 ] 𝜑
8		sbequ12r	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
9	8	sbcbidv	⊢ ( 𝑧 = 𝑦 → ( [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
10	6 7 9	cbvalv1	⊢ ( ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
11	3 4 10	3bitri	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )