Theorem sbcco

Description: A composition law for class substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker sbccow when possible. (Contributed by NM, 26-Sep-2003) (Revised by Mario Carneiro, 13-Oct-2016) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
2		sbcex	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
3		dfsbcq	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) )
4		dfsbcq	⊢ ( 𝑧 = 𝐴 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
5		sbsbc	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 )
6	5	sbbii	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 )
7		nfv	⊢ Ⅎ 𝑦 𝜑
8	7	sbco2	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
9		sbsbc	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 )
10	6 8 9	3bitr3ri	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
11		sbsbc	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
12	10 11	bitri	⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 )
13	3 4 12	vtoclbg	⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 ) )
14	1 2 13	pm5.21nii	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )