Theorem bj-cbv2v

Description: Version of cbv2 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 16-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-cbv2v.1	|- F/ x ph
	bj-cbv2v.2	|- F/ y ph
	bj-cbv2v.3	|- ( ph -> F/ y ps )
	bj-cbv2v.4	|- ( ph -> F/ x ch )
	bj-cbv2v.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion	bj-cbv2v	|- ( ph -> ( A. x ps <-> A. y ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-cbv2v.1	|- F/ x ph
2		bj-cbv2v.2	|- F/ y ph
3		bj-cbv2v.3	|- ( ph -> F/ y ps )
4		bj-cbv2v.4	|- ( ph -> F/ x ch )
5		bj-cbv2v.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
6	2	nf5ri	|- ( ph -> A. y ph )
7	1	nfal	|- F/ x A. y ph
8	7	nf5ri	|- ( A. y ph -> A. x A. y ph )
9	6 8	syl	|- ( ph -> A. x A. y ph )
10	3	nf5rd	|- ( ph -> ( ps -> A. y ps ) )
11	4	nf5rd	|- ( ph -> ( ch -> A. x ch ) )
12	10 11 5	bj-cbv2hv	|- ( A. x A. y ph -> ( A. x ps <-> A. y ch ) )
13	9 12	syl	|- ( ph -> ( A. x ps <-> A. y ch ) )