Theorem sbcal

Description: Move universal quantifier in and out of class substitution. (Contributed by NM, 31-Dec-2016) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcal	⊢ ( [ 𝐴 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑦 ] ∀ 𝑥 𝜑 → 𝐴 ∈ V )
2		sbcex	⊢ ( [ 𝐴 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
3	2	spsv	⊢ ( ∀ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
4		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ [ 𝐴 / 𝑦 ] ∀ 𝑥 𝜑 ) )
5		dfsbcq2	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] 𝜑 ) )
6	5	albidv	⊢ ( 𝑧 = 𝐴 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 ) )
7		sbal	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )
8	4 6 7	vtoclbg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 ) )
9	1 3 8	pm5.21nii	⊢ ( [ 𝐴 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝐴 / 𝑦 ] 𝜑 )