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 Gino Giotto, 10-Jan-2024)

Ref Expression
Assertion sbccow [˙A/y]˙[˙y/x]˙φ[˙A/x]˙φ

Proof

Step Hyp Ref Expression
1 sbcex [˙A/y]˙[˙y/x]˙φAV
2 sbcex [˙A/x]˙φAV
3 dfsbcq z=A[˙z/y]˙[˙y/x]˙φ[˙A/y]˙[˙y/x]˙φ
4 dfsbcq z=A[˙z/x]˙φ[˙A/x]˙φ
5 sbsbc yxφ[˙y/x]˙φ
6 5 sbbii zyyxφzy[˙y/x]˙φ
7 sbco2vv zyyxφzxφ
8 sbsbc zy[˙y/x]˙φ[˙z/y]˙[˙y/x]˙φ
9 6 7 8 3bitr3ri [˙z/y]˙[˙y/x]˙φzxφ
10 sbsbc zxφ[˙z/x]˙φ
11 9 10 bitri [˙z/y]˙[˙y/x]˙φ[˙z/x]˙φ
12 3 4 11 vtoclbg AV[˙A/y]˙[˙y/x]˙φ[˙A/x]˙φ
13 1 2 12 pm5.21nii [˙A/y]˙[˙y/x]˙φ[˙A/x]˙φ