Theorem cbvalv1

Description: Rule used to change bound variables, using implicit substitution. Version of cbval with a disjoint variable condition, which does not require ax-13 . See cbvalvw for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv for another variant. (Contributed by NM, 13-May-1993) (Revised by BJ, 31-May-2019)

	Ref	Expression
Hypotheses	cbvalv1.nf1	$$⊢Ⅎy\phi$$
	cbvalv1.nf2	$$⊢Ⅎx\psi$$
	cbvalv1.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvalv1	$$⊢\forall x\phi \leftrightarrow \forall y\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvalv1.nf1	$$⊢Ⅎy\phi$$
2		cbvalv1.nf2	$$⊢Ⅎx\psi$$
3		cbvalv1.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
4	3	biimpd	$$⊢x=y\to \left(\phi \to \psi \right)$$
5	1 2 4	cbv3v	$$⊢\forall x\phi \to \forall y\psi$$
6	3	biimprd	$$⊢x=y\to \left(\psi \to \phi \right)$$
7	6	equcoms	$$⊢y=x\to \left(\psi \to \phi \right)$$
8	2 1 7	cbv3v	$$⊢\forall y\psi \to \forall x\phi$$
9	5 8	impbii	$$⊢\forall x\phi \leftrightarrow \forall y\psi$$