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 } , (/) )