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		nfv	⊢ Ⅎ 𝑧 𝜑
3	2	sb8v	⊢ ( ∀ 𝑦 𝜑 ↔ ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
4	3	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 𝜑 ↔ [ 𝐴 / 𝑥 ] ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 )
5		sbcal	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑧 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
6		nfs1v	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
7	1 6	nfsbcw	⊢ Ⅎ 𝑦 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
8		nfv	⊢ Ⅎ 𝑧 [ 𝐴 / 𝑥 ] 𝜑
9		sbequ12r	⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
10	9	sbcbidv	⊢ ( 𝑧 = 𝑦 → ( [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
11	7 8 10	cbvalv1	⊢ ( ∀ 𝑧 [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )
12	4 5 11	3bitri	⊢ ( [ 𝐴 / 𝑥 ] ∀ 𝑦 𝜑 ↔ ∀ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 )