Theorem cbvreuw

Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreuw.1	|- F/ y ph
2		cbvreuw.2	|- F/ x ps
3		cbvreuw.3	|- ( x = y -> ( ph <-> ps ) )
4		nfv	|- F/ z ( x e. A /\ ph )
5	4	sb8euv	|- ( 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	nfsbv	|- 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	sbiev	|- ( [ 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	cbveuw	|- ( 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 )