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	|- F/_ y A
	cbvralcsf.2	|- F/_ x B
	cbvralcsf.3	|- F/ y ph
	cbvralcsf.4	|- F/ x ps
	cbvralcsf.5	|- ( x = y -> A = B )
	cbvralcsf.6	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvralcsf	|- ( A. x e. A ph <-> A. y e. B ps )

Proof

Step	Hyp	Ref	Expression
1		cbvralcsf.1	|- F/_ y A
2		cbvralcsf.2	|- F/_ x B
3		cbvralcsf.3	|- F/ y ph
4		cbvralcsf.4	|- F/ x ps
5		cbvralcsf.5	|- ( x = y -> A = B )
6		cbvralcsf.6	|- ( x = y -> ( ph <-> ps ) )
7		nfv	|- F/ z ( x e. A -> ph )
8		nfcsb1v	|- F/_ x [_ z / x ]_ A
9	8	nfcri	|- F/ x z e. [_ z / x ]_ A
10		nfsbc1v	|- F/ x [. z / x ]. ph
11	9 10	nfim	|- F/ x ( z e. [_ z / x ]_ A -> [. z / x ]. ph )
12		id	|- ( x = z -> x = z )
13		csbeq1a	|- ( x = z -> A = [_ z / x ]_ A )
14	12 13	eleq12d	|- ( x = z -> ( x e. A <-> z e. [_ z / x ]_ A ) )
15		sbceq1a	|- ( x = z -> ( ph <-> [. z / x ]. ph ) )
16	14 15	imbi12d	|- ( x = z -> ( ( x e. A -> ph ) <-> ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) ) )
17	7 11 16	cbvalv1	|- ( A. x ( x e. A -> ph ) <-> A. z ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) )
18		nfcv	|- F/_ y z
19	18 1	nfcsb	|- F/_ y [_ z / x ]_ A
20	19	nfcri	|- F/ y z e. [_ z / x ]_ A
21	18 3	nfsbc	|- F/ y [. z / x ]. ph
22	20 21	nfim	|- F/ y ( z e. [_ z / x ]_ A -> [. z / x ]. ph )
23		nfv	|- F/ z ( y e. B -> ps )
24		id	|- ( z = y -> z = y )
25		csbeq1	|- ( z = y -> [_ z / x ]_ A = [_ y / x ]_ A )
26		df-csb	|- [_ y / x ]_ A = { v | [. y / x ]. v e. A }
27	2	nfcri	|- F/ x v e. B
28	5	eleq2d	|- ( x = y -> ( v e. A <-> v e. B ) )
29	27 28	sbie	|- ( [ y / x ] v e. A <-> v e. B )
30		sbsbc	|- ( [ y / x ] v e. A <-> [. y / x ]. v e. A )
31	29 30	bitr3i	|- ( v e. B <-> [. y / x ]. v e. A )
32	31	abbi2i	|- B = { v | [. y / x ]. v e. A }
33	26 32	eqtr4i	|- [_ y / x ]_ A = B
34	25 33	eqtrdi	|- ( z = y -> [_ z / x ]_ A = B )
35	24 34	eleq12d	|- ( z = y -> ( z e. [_ z / x ]_ A <-> y e. B ) )
36		dfsbcq	|- ( z = y -> ( [. z / x ]. ph <-> [. y / x ]. ph ) )
37		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
38	4 6	sbie	|- ( [ y / x ] ph <-> ps )
39	37 38	bitr3i	|- ( [. y / x ]. ph <-> ps )
40	36 39	bitrdi	|- ( z = y -> ( [. z / x ]. ph <-> ps ) )
41	35 40	imbi12d	|- ( z = y -> ( ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) <-> ( y e. B -> ps ) ) )
42	22 23 41	cbvalv1	|- ( A. z ( z e. [_ z / x ]_ A -> [. z / x ]. ph ) <-> A. y ( y e. B -> ps ) )
43	17 42	bitri	|- ( A. x ( x e. A -> ph ) <-> A. y ( y e. B -> ps ) )
44		df-ral	|- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
45		df-ral	|- ( A. y e. B ps <-> A. y ( y e. B -> ps ) )
46	43 44 45	3bitr4i	|- ( A. x e. A ph <-> A. y e. B ps )