Theorem sbco2v

Description: A composition law for substitution. Version of sbco2 with disjoint variable conditions, not requiring ax-13 , but ax-11 . (Contributed by NM, 30-Jun-1994) (Revised by Wolf Lammen, 29-Apr-2023)

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

Proof

Step	Hyp	Ref	Expression
1		sbco2v.1	|- F/ z ph
2	1	nfsbv	|- F/ z [ y / x ] ph
3		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
4	2 3	sbiev	|- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )