This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbccow

Description: A composition law for class substitution. Version of sbcco with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 26-Sep-2003) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

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

Proof

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