Theorem cbvrexcsf

Description: A more general version of cbvrexf that has no distinct variable restrictions. 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) (Proof shortened by Mario Carneiro, 7-Dec-2014) (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	cbvrexcsf	|- ( E. x e. A ph <-> E. 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	3	nfn	|- F/ y -. ph
8	4	nfn	|- F/ x -. ps
9	6	notbid	|- ( x = y -> ( -. ph <-> -. ps ) )
10	1 2 7 8 5 9	cbvralcsf	|- ( A. x e. A -. ph <-> A. y e. B -. ps )
11	10	notbii	|- ( -. A. x e. A -. ph <-> -. A. y e. B -. ps )
12		dfrex2	|- ( E. x e. A ph <-> -. A. x e. A -. ph )
13		dfrex2	|- ( E. y e. B ps <-> -. A. y e. B -. ps )
14	11 12 13	3bitr4i	|- ( E. x e. A ph <-> E. y e. B ps )