Description: Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | difmapsn.a | |
|
difmapsn.b | |
||
difmapsn.v | |
||
Assertion | difmapsn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | difmapsn.a | |
|
2 | difmapsn.b | |
|
3 | difmapsn.v | |
|
4 | eldifi | |
|
5 | 4 | adantl | |
6 | elmapi | |
|
7 | 6 | adantl | |
8 | fsn2g | |
|
9 | 3 8 | syl | |
10 | 9 | adantr | |
11 | 7 10 | mpbid | |
12 | 11 | simpld | |
13 | 5 12 | syldan | |
14 | simpr | |
|
15 | 11 | simprd | |
16 | 5 15 | syldan | |
17 | 16 | adantr | |
18 | 14 17 | jca | |
19 | fsn2g | |
|
20 | 3 19 | syl | |
21 | 20 | ad2antrr | |
22 | 18 21 | mpbird | |
23 | 2 | ad2antrr | |
24 | snex | |
|
25 | 24 | a1i | |
26 | 23 25 | elmapd | |
27 | 22 26 | mpbird | |
28 | eldifn | |
|
29 | 28 | ad2antlr | |
30 | 27 29 | pm2.65da | |
31 | 13 30 | eldifd | |
32 | 31 16 | jca | |
33 | fsn2g | |
|
34 | 3 33 | syl | |
35 | 34 | adantr | |
36 | 32 35 | mpbird | |
37 | difssd | |
|
38 | 1 37 | ssexd | |
39 | 24 | a1i | |
40 | 38 39 | elmapd | |
41 | 40 | adantr | |
42 | 36 41 | mpbird | |
43 | 42 | ralrimiva | |
44 | dfss3 | |
|
45 | 43 44 | sylibr | |
46 | 3 | snn0d | |
47 | 1 2 39 46 | difmap | |
48 | 45 47 | eqssd | |