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) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024) Avoid ax-10 . (Revised by Wolf Lammen, 10-Dec-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	1 2 3	cbvrexw	|- ( E. x e. A ph <-> E. y e. A ps )
5	1 2 3	cbvrmow	|- ( E* x e. A ph <-> E* y e. A ps )
6	4 5	anbi12i	|- ( ( E. x e. A ph /\ E* x e. A ph ) <-> ( E. y e. A ps /\ E* y e. A ps ) )
7		reu5	|- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
8		reu5	|- ( E! y e. A ps <-> ( E. y e. A ps /\ E* y e. A ps ) )
9	6 7 8	3bitr4i	|- ( E! x e. A ph <-> E! y e. A ps )