Theorem cbveud

Description: Deduction used to change bound variables in an existential uniqueness quantifier, using implicit substitution. (Contributed by ML, 27-Mar-2021)

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

Proof

Step	Hyp	Ref	Expression
1		cbveud.1	|- F/ x ph
2		cbveud.2	|- F/ y ph
3		cbveud.3	|- ( ph -> F/ y ps )
4		cbveud.4	|- ( ph -> F/ x ch )
5		cbveud.5	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
6		nfvd	|- ( ph -> F/ y x = z )
7	3 6	nfbid	|- ( ph -> F/ y ( ps <-> x = z ) )
8		nfvd	|- ( ph -> F/ x y = z )
9	4 8	nfbid	|- ( ph -> F/ x ( ch <-> y = z ) )
10		simpr	|- ( ( x = y /\ ( ps <-> ch ) ) -> ( ps <-> ch ) )
11		equequ1	|- ( x = y -> ( x = z <-> y = z ) )
12	11	adantr	|- ( ( x = y /\ ( ps <-> ch ) ) -> ( x = z <-> y = z ) )
13	10 12	bibi12d	|- ( ( x = y /\ ( ps <-> ch ) ) -> ( ( ps <-> x = z ) <-> ( ch <-> y = z ) ) )
14	13	ex	|- ( x = y -> ( ( ps <-> ch ) -> ( ( ps <-> x = z ) <-> ( ch <-> y = z ) ) ) )
15	5 14	sylcom	|- ( ph -> ( x = y -> ( ( ps <-> x = z ) <-> ( ch <-> y = z ) ) ) )
16	1 2 7 9 15	cbv2w	|- ( ph -> ( A. x ( ps <-> x = z ) <-> A. y ( ch <-> y = z ) ) )
17	16	exbidv	|- ( ph -> ( E. z A. x ( ps <-> x = z ) <-> E. z A. y ( ch <-> y = z ) ) )
18		eu6	|- ( E! x ps <-> E. z A. x ( ps <-> x = z ) )
19		eu6	|- ( E! y ch <-> E. z A. y ( ch <-> y = z ) )
20	17 18 19	3bitr4g	|- ( ph -> ( E! x ps <-> E! y ch ) )