Theorem cbvralf

Description: Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvralfw when possible. (Contributed by NM, 7-Mar-2004) (Revised by Mario Carneiro, 9-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvralf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	cbvralf.2	$$⊢\underset{\_}{Ⅎ}yA$$
	cbvralf.3	$$⊢Ⅎy\phi$$
	cbvralf.4	$$⊢Ⅎx\psi$$
	cbvralf.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	cbvralf	$$⊢\forall x\in A\phi \leftrightarrow \forall y\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		cbvralf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		cbvralf.2	$$⊢\underset{\_}{Ⅎ}yA$$
3		cbvralf.3	$$⊢Ⅎy\phi$$
4		cbvralf.4	$$⊢Ⅎx\psi$$
5		cbvralf.5	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
6		nfv	$$⊢Ⅎz\left(x\in A\to \phi \right)$$
7	1	nfcri	$$⊢Ⅎxz\in A$$
8		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
9	7 8	nfim	$$⊢Ⅎx\left(z\in A\to \left[z/x\right]\phi \right)$$
10		eleq1w	$$⊢x=z\to \left(x\in A\leftrightarrow z\in A\right)$$
11		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
12	10 11	imbi12d	$$⊢x=z\to \left(\left(x\in A\to \phi \right)\leftrightarrow \left(z\in A\to \left[z/x\right]\phi \right)\right)$$
13	6 9 12	cbvalv1	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall z\left(z\in A\to \left[z/x\right]\phi \right)$$
14	2	nfcri	$$⊢Ⅎyz\in A$$
15	3	nfsb	$$⊢Ⅎy\left[z/x\right]\phi$$
16	14 15	nfim	$$⊢Ⅎy\left(z\in A\to \left[z/x\right]\phi \right)$$
17		nfv	$$⊢Ⅎz\left(y\in A\to \psi \right)$$
18		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
19		sbequ	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
20	4 5	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
21	19 20	bitrdi	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \psi \right)$$
22	18 21	imbi12d	$$⊢z=y\to \left(\left(z\in A\to \left[z/x\right]\phi \right)\leftrightarrow \left(y\in A\to \psi \right)\right)$$
23	16 17 22	cbvalv1	$$⊢\forall z\left(z\in A\to \left[z/x\right]\phi \right)\leftrightarrow \forall y\left(y\in A\to \psi \right)$$
24	13 23	bitri	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall y\left(y\in A\to \psi \right)$$
25		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
26		df-ral	$$⊢\forall y\in A\psi \leftrightarrow \forall y\left(y\in A\to \psi \right)$$
27	24 25 26	3bitr4i	$$⊢\forall x\in A\phi \leftrightarrow \forall y\in A\psi$$