Theorem reurab

Description: Restricted existential uniqueness of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Hypothesis	reurab.1	|- ( x = y -> ( ph <-> ps ) )
Assertion	reurab	|- ( E! x e. { y e. A | ps } ch <-> E! x e. A ( ph /\ ch ) )

Proof

Step	Hyp	Ref	Expression
1		reurab.1	|- ( x = y -> ( ph <-> ps ) )
2	1	bicomd	|- ( x = y -> ( ps <-> ph ) )
3	2	equcoms	|- ( y = x -> ( ps <-> ph ) )
4	3	elrab	|- ( x e. { y e. A | ps } <-> ( x e. A /\ ph ) )
5	4	anbi1i	|- ( ( x e. { y e. A | ps } /\ ch ) <-> ( ( x e. A /\ ph ) /\ ch ) )
6		anass	|- ( ( ( x e. A /\ ph ) /\ ch ) <-> ( x e. A /\ ( ph /\ ch ) ) )
7	5 6	bitri	|- ( ( x e. { y e. A | ps } /\ ch ) <-> ( x e. A /\ ( ph /\ ch ) ) )
8	7	eubii	|- ( E! x ( x e. { y e. A | ps } /\ ch ) <-> E! x ( x e. A /\ ( ph /\ ch ) ) )
9		df-reu	|- ( E! x e. { y e. A | ps } ch <-> E! x ( x e. { y e. A | ps } /\ ch ) )
10		df-reu	|- ( E! x e. A ( ph /\ ch ) <-> E! x ( x e. A /\ ( ph /\ ch ) ) )
11	8 9 10	3bitr4i	|- ( E! x e. { y e. A | ps } ch <-> E! x e. A ( ph /\ ch ) )