This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )