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	$$⊢Ⅎx\phi$$
	bj-cbv2v.2	$$⊢Ⅎy\phi$$
	bj-cbv2v.3	$$⊢\phi \to Ⅎy\psi$$
	bj-cbv2v.4	$$⊢\phi \to Ⅎx\chi$$
	bj-cbv2v.5	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
Assertion	bj-cbv2v	$$⊢\phi \to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-cbv2v.1	$$⊢Ⅎx\phi$$
2		bj-cbv2v.2	$$⊢Ⅎy\phi$$
3		bj-cbv2v.3	$$⊢\phi \to Ⅎy\psi$$
4		bj-cbv2v.4	$$⊢\phi \to Ⅎx\chi$$
5		bj-cbv2v.5	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
6	2	nf5ri	$$⊢\phi \to \forall y\phi$$
7	1	nfal	$$⊢Ⅎx\forall y\phi$$
8	7	nf5ri	$$⊢\forall y\phi \to \forall x\forall y\phi$$
9	6 8	syl	$$⊢\phi \to \forall x\forall y\phi$$
10	3	nf5rd	$$⊢\phi \to \left(\psi \to \forall y\psi \right)$$
11	4	nf5rd	$$⊢\phi \to \left(\chi \to \forall x\chi \right)$$
12	10 11 5	bj-cbv2hv	$$⊢\forall x\forall y\phi \to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$
13	9 12	syl	$$⊢\phi \to \left(\forall x\psi \leftrightarrow \forall y\chi \right)$$