Theorem cbvralcsf

Description: A more general version of cbvralf that doesn't require A and B to be distinct from x or y . Changes bound variables using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 13-Jul-2011) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	$$⊢\underset{\_}{Ⅎ}yA$$
2		cbvralcsf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		cbvralcsf.3	$$⊢Ⅎy\phi$$
4		cbvralcsf.4	$$⊢Ⅎx\psi$$
5		cbvralcsf.5	$$⊢x=y\to A=B$$
6		cbvralcsf.6	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
7		nfv	$$⊢Ⅎz\left(x\in A\to \phi \right)$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌A$$
9	8	nfcri	$$⊢Ⅎxz\in ⦋z/x⦌A$$
10		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
11	9 10	nfim	$$⊢Ⅎx\left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
12		id	$$⊢x=z\to x=z$$
13		csbeq1a	$$⊢x=z\to A=⦋z/x⦌A$$
14	12 13	eleq12d	$$⊢x=z\to \left(x\in A\leftrightarrow z\in ⦋z/x⦌A\right)$$
15		sbceq1a	$$⊢x=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
16	14 15	imbi12d	$$⊢x=z\to \left(\left(x\in A\to \phi \right)\leftrightarrow \left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\right)$$
17	7 11 16	cbvalv1	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall z\left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
19	18 1	nfcsb	$$⊢\underset{\_}{Ⅎ}y⦋z/x⦌A$$
20	19	nfcri	$$⊢Ⅎyz\in ⦋z/x⦌A$$
21	18 3	nfsbc	$$⊢Ⅎy\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
22	20 21	nfim	$$⊢Ⅎy\left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
23		nfv	$$⊢Ⅎz\left(y\in B\to \psi \right)$$
24		id	$$⊢z=y\to z=y$$
25		csbeq1	$$⊢z=y\to ⦋z/x⦌A=⦋y/x⦌A$$
26		df-csb	$$⊢⦋y/x⦌A=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
27	2	nfcri	$$⊢Ⅎxv\in B$$
28	5	eleq2d	$$⊢x=y\to \left(v\in A\leftrightarrow v\in B\right)$$
29	27 28	sbie	$$⊢\left[y/x\right]v\in A\leftrightarrow v\in B$$
30		sbsbc	$$⊢\left[y/x\right]v\in A\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A$$
31	29 30	bitr3i	$$⊢v\in B\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A$$
32	31	eqabi	$$⊢B=\left\{v|\underset{\dot{}}{[}y/x\underset{\dot{}}{]}v\in A\right\}$$
33	26 32	eqtr4i	$$⊢⦋y/x⦌A=B$$
34	25 33	eqtrdi	$$⊢z=y\to ⦋z/x⦌A=B$$
35	24 34	eleq12d	$$⊢z=y\to \left(z\in ⦋z/x⦌A\leftrightarrow y\in B\right)$$
36		dfsbcq	$$⊢z=y\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
37		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
38	4 6	sbie	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
39	37 38	bitr3i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
40	36 39	bitrdi	$$⊢z=y\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
41	35 40	imbi12d	$$⊢z=y\to \left(\left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(y\in B\to \psi \right)\right)$$
42	22 23 41	cbvalv1	$$⊢\forall z\left(z\in ⦋z/x⦌A\to \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \forall y\left(y\in B\to \psi \right)$$
43	17 42	bitri	$$⊢\forall x\left(x\in A\to \phi \right)\leftrightarrow \forall y\left(y\in B\to \psi \right)$$
44		df-ral	$$⊢\forall x\in A\phi \leftrightarrow \forall x\left(x\in A\to \phi \right)$$
45		df-ral	$$⊢\forall y\in B\psi \leftrightarrow \forall y\left(y\in B\to \psi \right)$$
46	43 44 45	3bitr4i	$$⊢\forall x\in A\phi \leftrightarrow \forall y\in B\psi$$