Theorem sbco2

Description: A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v and sbco2vv . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 30-Jun-1994) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 17-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbco2.1	|- F/ z ph
Assertion	sbco2	|- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		sbco2.1	|- F/ z ph
2		sbequ12	|- ( z = y -> ( [ z / x ] ph <-> [ y / z ] [ z / x ] ph ) )
3		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
4	2 3	bitr3d	|- ( z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
5	4	sps	|- ( A. z z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
6		nfnae	|- F/ z -. A. z z = y
7	1	nfsb4	|- ( -. A. z z = y -> F/ z [ y / x ] ph )
8	3	a1i	|- ( -. A. z z = y -> ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) ) )
9	6 7 8	sbied	|- ( -. A. z z = y -> ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph ) )
10	5 9	pm2.61i	|- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )