Theorem csbab

Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005) (Revised by NM, 19-Aug-2018)

	Ref	Expression
Assertion	csbab	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
2		sbsbc	⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
3	1 2	bitri	⊢ ( 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } ↔ [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )
4		sbccom	⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
5		df-clab	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
6		sbsbc	⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 )
7	5 6	bitri	⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
8	7	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝐴 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 )
9	4 8	bitr4i	⊢ ( [ 𝑧 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } )
10		sbcel2	⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } )
11	3 9 10	3bitrri	⊢ ( 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 } )
12	11	eqriv	⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ 𝜑 } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] 𝜑 }