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 ⊢ [˙A / y]˙ [˙y / x]˙ φ ↔ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / y]˙ [˙y / x]˙ φ → A ∈ V
2 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
3 dfsbcq ⊢ z = A → [˙z / y]˙ [˙y / x]˙ φ ↔ [˙A / y]˙ [˙y / x]˙ φ
4 dfsbcq ⊢ z = A → [˙z / x]˙ φ ↔ [˙A / x]˙ φ
5 sbsbc ⊢ y x φ ↔ [˙y / x]˙ φ
6 5 sbbii ⊢ z y y x φ ↔ z y [˙y / x]˙ φ
7 nfv ⊢ Ⅎ y φ
8 7 sbco2 ⊢ z y y x φ ↔ z x φ
9 sbsbc ⊢ z y [˙y / x]˙ φ ↔ [˙z / y]˙ [˙y / x]˙ φ
10 6 8 9 3bitr3ri ⊢ [˙z / y]˙ [˙y / x]˙ φ ↔ z x φ
11 sbsbc ⊢ z x φ ↔ [˙z / x]˙ φ
12 10 11 bitri ⊢ [˙z / y]˙ [˙y / x]˙ φ ↔ [˙z / x]˙ φ
13 3 4 12 vtoclbg ⊢ A ∈ V → [˙A / y]˙ [˙y / x]˙ φ ↔ [˙A / x]˙ φ
14 1 2 13 pm5.21nii ⊢ [˙A / y]˙ [˙y / x]˙ φ ↔ [˙A / x]˙ φ