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 A | φ = if [˙A / x]˙ φ A

Proof

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