Metamath Proof Explorer

Theorem rabsnifsb

Description: A restricted class abstraction restricted to a singleton is either the empty set or the singleton itself. (Contributed by AV, 21-Jul-2019)

Ref Expression
Assertion rabsnifsb 
|- { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )

Proof

Step Hyp Ref Expression
1 elsni 
 |-  ( x e. { A } -> x = A )
2 sbceq1a 
 |-  ( x = A -> ( ph <-> [. A / x ]. ph ) )
3 2 biimpd 
 |-  ( x = A -> ( ph -> [. A / x ]. ph ) )
4 1 3 syl 
 |-  ( x e. { A } -> ( ph -> [. A / x ]. ph ) )
5 4 imdistani 
 |-  ( ( x e. { A } /\ ph ) -> ( x e. { A } /\ [. A / x ]. ph ) )
6 5 orcd 
 |-  ( ( x e. { A } /\ ph ) -> ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) )
7 2 biimprd 
 |-  ( x = A -> ( [. A / x ]. ph -> ph ) )
8 1 7 syl 
 |-  ( x e. { A } -> ( [. A / x ]. ph -> ph ) )
9 8 imdistani 
 |-  ( ( x e. { A } /\ [. A / x ]. ph ) -> ( x e. { A } /\ ph ) )
10 noel 
 |-  -. x e. (/)
11 10 pm2.21i 
 |-  ( x e. (/) -> ( x e. { A } /\ ph ) )
12 11 adantr 
 |-  ( ( x e. (/) /\ -. [. A / x ]. ph ) -> ( x e. { A } /\ ph ) )
13 9 12 jaoi 
 |-  ( ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) -> ( x e. { A } /\ ph ) )
14 6 13 impbii 
 |-  ( ( x e. { A } /\ ph ) <-> ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) )
15 14 abbii 
 |-  { x | ( x e. { A } /\ ph ) } = { x | ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) }
16 nfv 
 |-  F/ y ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) )
17 nfv 
 |-  F/ x y e. { A }
18 nfsbc1v 
 |-  F/ x [. A / x ]. ph
19 17 18 nfan 
 |-  F/ x ( y e. { A } /\ [. A / x ]. ph )
20 nfv 
 |-  F/ x y e. (/)
21 18 nfn 
 |-  F/ x -. [. A / x ]. ph
22 20 21 nfan 
 |-  F/ x ( y e. (/) /\ -. [. A / x ]. ph )
23 19 22 nfor 
 |-  F/ x ( ( y e. { A } /\ [. A / x ]. ph ) \/ ( y e. (/) /\ -. [. A / x ]. ph ) )
24 eleq1w 
 |-  ( x = y -> ( x e. { A } <-> y e. { A } ) )
25 24 anbi1d 
 |-  ( x = y -> ( ( x e. { A } /\ [. A / x ]. ph ) <-> ( y e. { A } /\ [. A / x ]. ph ) ) )
26 eleq1w 
 |-  ( x = y -> ( x e. (/) <-> y e. (/) ) )
27 26 anbi1d 
 |-  ( x = y -> ( ( x e. (/) /\ -. [. A / x ]. ph ) <-> ( y e. (/) /\ -. [. A / x ]. ph ) ) )
28 25 27 orbi12d 
 |-  ( x = y -> ( ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) <-> ( ( y e. { A } /\ [. A / x ]. ph ) \/ ( y e. (/) /\ -. [. A / x ]. ph ) ) ) )
29 16 23 28 cbvabw 
 |-  { x | ( ( x e. { A } /\ [. A / x ]. ph ) \/ ( x e. (/) /\ -. [. A / x ]. ph ) ) } = { y | ( ( y e. { A } /\ [. A / x ]. ph ) \/ ( y e. (/) /\ -. [. A / x ]. ph ) ) }
30 15 29 eqtri 
 |-  { x | ( x e. { A } /\ ph ) } = { y | ( ( y e. { A } /\ [. A / x ]. ph ) \/ ( y e. (/) /\ -. [. A / x ]. ph ) ) }
31 df-rab 
 |-  { x e. { A } | ph } = { x | ( x e. { A } /\ ph ) }
32 df-if 
 |-  if ( [. A / x ]. ph , { A } , (/) ) = { y | ( ( y e. { A } /\ [. A / x ]. ph ) \/ ( y e. (/) /\ -. [. A / x ]. ph ) ) }
33 30 31 32 3eqtr4i 
 |-  { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )