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

Metamath Proof Explorer

Theorem rabsnif

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

Ref Expression
Hypothesis rabsnif.f 
|- ( x = A -> ( ph <-> ps ) )
Assertion rabsnif 
|- { x e. { A } | ph } = if ( ps , { A } , (/) )

Proof

Step Hyp Ref Expression
1 rabsnif.f 
 |-  ( x = A -> ( ph <-> ps ) )
2 rabsnifsb 
 |-  { x e. { A } | ph } = if ( [. A / x ]. ph , { A } , (/) )
3 1 sbcieg 
 |-  ( A e. _V -> ( [. A / x ]. ph <-> ps ) )
4 3 ifbid 
 |-  ( A e. _V -> if ( [. A / x ]. ph , { A } , (/) ) = if ( ps , { A } , (/) ) )
5 2 4 eqtrid 
 |-  ( A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) )
6 rab0 
 |-  { x e. (/) | ph } = (/)
7 ifid 
 |-  if ( ps , (/) , (/) ) = (/)
8 6 7 eqtr4i 
 |-  { x e. (/) | ph } = if ( ps , (/) , (/) )
9 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
10 9 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
11 10 rabeqdv 
 |-  ( -. A e. _V -> { x e. { A } | ph } = { x e. (/) | ph } )
12 10 ifeq1d 
 |-  ( -. A e. _V -> if ( ps , { A } , (/) ) = if ( ps , (/) , (/) ) )
13 8 11 12 3eqtr4a 
 |-  ( -. A e. _V -> { x e. { A } | ph } = if ( ps , { A } , (/) ) )
14 5 13 pm2.61i 
 |-  { x e. { A } | ph } = if ( ps , { A } , (/) )