Theorem rabeqsnd

Description: Conditions for a restricted class abstraction to be a singleton, in deduction form. (Contributed by Thierry Arnoux, 2-Dec-2021)

	Ref	Expression
Hypotheses	rabeqsnd.0	|- ( x = B -> ( ps <-> ch ) )
	rabeqsnd.1	|- ( ph -> B e. A )
	rabeqsnd.2	|- ( ph -> ch )
	rabeqsnd.3	|- ( ( ( ph /\ x e. A ) /\ ps ) -> x = B )
Assertion	rabeqsnd	|- ( ph -> { x e. A | ps } = { B } )

Proof

Step	Hyp	Ref	Expression
1		rabeqsnd.0	|- ( x = B -> ( ps <-> ch ) )
2		rabeqsnd.1	|- ( ph -> B e. A )
3		rabeqsnd.2	|- ( ph -> ch )
4		rabeqsnd.3	|- ( ( ( ph /\ x e. A ) /\ ps ) -> x = B )
5	4	expl	|- ( ph -> ( ( x e. A /\ ps ) -> x = B ) )
6	5	alrimiv	|- ( ph -> A. x ( ( x e. A /\ ps ) -> x = B ) )
7	2 3	jca	|- ( ph -> ( B e. A /\ ch ) )
8	7	a1d	|- ( ph -> ( x = B -> ( B e. A /\ ch ) ) )
9	8	alrimiv	|- ( ph -> A. x ( x = B -> ( B e. A /\ ch ) ) )
10		eleq1	|- ( x = B -> ( x e. A <-> B e. A ) )
11	10 1	anbi12d	|- ( x = B -> ( ( x e. A /\ ps ) <-> ( B e. A /\ ch ) ) )
12	11	pm5.74i	|- ( ( x = B -> ( x e. A /\ ps ) ) <-> ( x = B -> ( B e. A /\ ch ) ) )
13	12	albii	|- ( A. x ( x = B -> ( x e. A /\ ps ) ) <-> A. x ( x = B -> ( B e. A /\ ch ) ) )
14	9 13	sylibr	|- ( ph -> A. x ( x = B -> ( x e. A /\ ps ) ) )
15	6 14	jca	|- ( ph -> ( A. x ( ( x e. A /\ ps ) -> x = B ) /\ A. x ( x = B -> ( x e. A /\ ps ) ) ) )
16		albiim	|- ( A. x ( ( x e. A /\ ps ) <-> x = B ) <-> ( A. x ( ( x e. A /\ ps ) -> x = B ) /\ A. x ( x = B -> ( x e. A /\ ps ) ) ) )
17	15 16	sylibr	|- ( ph -> A. x ( ( x e. A /\ ps ) <-> x = B ) )
18		rabeqsn	|- ( { x e. A | ps } = { B } <-> A. x ( ( x e. A /\ ps ) <-> x = B ) )
19	17 18	sylibr	|- ( ph -> { x e. A | ps } = { B } )