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	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcex	|- ( [. A / y ]. [. y / x ]. ph -> A e. _V )
2		sbcex	|- ( [. A / x ]. ph -> A e. _V )
3		dfsbcq	|- ( z = A -> ( [. z / y ]. [. y / x ]. ph <-> [. A / y ]. [. y / x ]. ph ) )
4		dfsbcq	|- ( z = A -> ( [. z / x ]. ph <-> [. A / x ]. ph ) )
5		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
6	5	sbbii	|- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [. y / x ]. ph )
7		sbco2vv	|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] ph )
8		sbsbc	|- ( [ z / y ] [. y / x ]. ph <-> [. z / y ]. [. y / x ]. ph )
9	6 7 8	3bitr3ri	|- ( [. z / y ]. [. y / x ]. ph <-> [ z / x ] ph )
10		sbsbc	|- ( [ z / x ] ph <-> [. z / x ]. ph )
11	9 10	bitri	|- ( [. z / y ]. [. y / x ]. ph <-> [. z / x ]. ph )
12	3 4 11	vtoclbg	|- ( A e. _V -> ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph ) )
13	1 2 12	pm5.21nii	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )