Theorem sbcco2

Description: A composition law for class substitution. Importantly, x may occur free in the class expression substituted for A . (Contributed by NM, 5-Sep-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Hypothesis	sbcco2.1	|- ( x = y -> A = B )
Assertion	sbcco2	|- ( [. x / y ]. [. B / x ]. ph <-> [. A / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbcco2.1	|- ( x = y -> A = B )
2		sbsbc	|- ( [ x / y ] [. B / x ]. ph <-> [. x / y ]. [. B / x ]. ph )
3	1	equcoms	|- ( y = x -> A = B )
4		dfsbcq	|- ( A = B -> ( [. A / x ]. ph <-> [. B / x ]. ph ) )
5	4	bicomd	|- ( A = B -> ( [. B / x ]. ph <-> [. A / x ]. ph ) )
6	3 5	syl	|- ( y = x -> ( [. B / x ]. ph <-> [. A / x ]. ph ) )
7	6	sbievw	|- ( [ x / y ] [. B / x ]. ph <-> [. A / x ]. ph )
8	2 7	bitr3i	|- ( [. x / y ]. [. B / x ]. ph <-> [. A / x ]. ph )