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 ]. 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		nfv	|- F/ y ph
8	7	sbco2	|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] ph )
9		sbsbc	|- ( [ z / y ] [. y / x ]. ph <-> [. z / y ]. [. y / x ]. ph )
10	6 8 9	3bitr3ri	|- ( [. z / y ]. [. y / x ]. ph <-> [ z / x ] ph )
11		sbsbc	|- ( [ z / x ] ph <-> [. z / x ]. ph )
12	10 11	bitri	|- ( [. z / y ]. [. y / x ]. ph <-> [. z / x ]. ph )
13	3 4 12	vtoclbg	|- ( A e. _V -> ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph ) )
14	1 2 13	pm5.21nii	|- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph )