Theorem cbvreud

Description: Deduction used to change bound variables in a restricted existential uniqueness quantifier. (Contributed by ML, 27-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cbvreud.1	|- F/ x ph
2		cbvreud.2	|- F/ y ph
3		cbvreud.3	|- ( ph -> F/ y ps )
4		cbvreud.4	|- ( ph -> F/ x ch )
5		cbvreud.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
6		nfvd	|- ( ph -> F/ y x e. A )
7	6 3	nfand	|- ( ph -> F/ y ( x e. A /\ ps ) )
8		nfvd	|- ( ph -> F/ x y e. A )
9	8 4	nfand	|- ( ph -> F/ x ( y e. A /\ ch ) )
10		eleq1	|- ( x = y -> ( x e. A <-> y e. A ) )
11	10	adantl	|- ( ( ph /\ x = y ) -> ( x e. A <-> y e. A ) )
12	5	imp	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
13	11 12	anbi12d	|- ( ( ph /\ x = y ) -> ( ( x e. A /\ ps ) <-> ( y e. A /\ ch ) ) )
14	13	ex	|- ( ph -> ( x = y -> ( ( x e. A /\ ps ) <-> ( y e. A /\ ch ) ) ) )
15	1 2 7 9 14	cbveud	|- ( ph -> ( E! x ( x e. A /\ ps ) <-> E! y ( y e. A /\ ch ) ) )
16		df-reu	|- ( E! x e. A ps <-> E! x ( x e. A /\ ps ) )
17		df-reu	|- ( E! y e. A ch <-> E! y ( y e. A /\ ch ) )
18	15 16 17	3bitr4g	|- ( ph -> ( E! x e. A ps <-> E! y e. A ch ) )