# 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) (Revised by Gino Giotto, 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 ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑[ 𝐴 / 𝑥 ] 𝜑 )