Theorem cbvreu

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvreuw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cbvral.1	|- F/ y ph
	cbvral.2	|- F/ x ps
	cbvral.3	|- ( x = y -> ( ph <-> ps ) )
Assertion	cbvreu	|- ( E! x e. A ph <-> E! y e. A ps )

Proof

Step	Hyp	Ref	Expression
1		cbvral.1	|- F/ y ph
2		cbvral.2	|- F/ x ps
3		cbvral.3	|- ( x = y -> ( ph <-> ps ) )
4		nfv	|- F/ z ( x e. A /\ ph )
5	4	sb8eu	|- ( E! x ( x e. A /\ ph ) <-> E! z [ z / x ] ( x e. A /\ ph ) )
6		sban	|- ( [ z / x ] ( x e. A /\ ph ) <-> ( [ z / x ] x e. A /\ [ z / x ] ph ) )
7	6	eubii	|- ( E! z [ z / x ] ( x e. A /\ ph ) <-> E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) )
8		clelsb1	|- ( [ z / x ] x e. A <-> z e. A )
9	8	anbi1i	|- ( ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> ( z e. A /\ [ z / x ] ph ) )
10	9	eubii	|- ( E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> E! z ( z e. A /\ [ z / x ] ph ) )
11		nfv	|- F/ y z e. A
12	1	nfsb	|- F/ y [ z / x ] ph
13	11 12	nfan	|- F/ y ( z e. A /\ [ z / x ] ph )
14		nfv	|- F/ z ( y e. A /\ ps )
15		eleq1w	|- ( z = y -> ( z e. A <-> y e. A ) )
16		sbequ	|- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
17	2 3	sbie	|- ( [ y / x ] ph <-> ps )
18	16 17	bitrdi	|- ( z = y -> ( [ z / x ] ph <-> ps ) )
19	15 18	anbi12d	|- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
20	13 14 19	cbveu	|- ( E! z ( z e. A /\ [ z / x ] ph ) <-> E! y ( y e. A /\ ps ) )
21	10 20	bitri	|- ( E! z ( [ z / x ] x e. A /\ [ z / x ] ph ) <-> E! y ( y e. A /\ ps ) )
22	5 7 21	3bitri	|- ( E! x ( x e. A /\ ph ) <-> E! y ( y e. A /\ ps ) )
23		df-reu	|- ( E! x e. A ph <-> E! x ( x e. A /\ ph ) )
24		df-reu	|- ( E! y e. A ps <-> E! y ( y e. A /\ ps ) )
25	22 23 24	3bitr4i	|- ( E! x e. A ph <-> E! y e. A ps )