Theorem bj-cbv3hv2

Description: Version of cbv3h with two disjoint variable conditions, which does not require ax-11 nor ax-13 . (Contributed by BJ, 24-Jun-2019) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-cbv3hv2.nf	|- ( ps -> A. x ps )
	bj-cbv3hv2.1	|- ( x = y -> ( ph -> ps ) )
Assertion	bj-cbv3hv2	|- ( A. x ph -> A. y ps )

Proof

Step	Hyp	Ref	Expression
1		bj-cbv3hv2.nf	|- ( ps -> A. x ps )
2		bj-cbv3hv2.1	|- ( x = y -> ( ph -> ps ) )
3	1	nf5i	|- F/ x ps
4	3 2	cbv3v2	|- ( A. x ph -> A. y ps )