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

Metamath Proof Explorer

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 ⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝐴 / 𝑥 ] 𝜑 )