Metamath Proof Explorer


Theorem difmapsn

Description: Difference of two sets exponentiatiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses difmapsn.a φAV
difmapsn.b φBW
difmapsn.v φCZ
Assertion difmapsn φACBC=ABC

Proof

Step Hyp Ref Expression
1 difmapsn.a φAV
2 difmapsn.b φBW
3 difmapsn.v φCZ
4 eldifi fACBCfAC
5 4 adantl φfACBCfAC
6 elmapi fACf:CA
7 6 adantl φfACf:CA
8 fsn2g CZf:CAfCAf=CfC
9 3 8 syl φf:CAfCAf=CfC
10 9 adantr φfACf:CAfCAf=CfC
11 7 10 mpbid φfACfCAf=CfC
12 11 simpld φfACfCA
13 5 12 syldan φfACBCfCA
14 simpr φfACBCfCBfCB
15 11 simprd φfACf=CfC
16 5 15 syldan φfACBCf=CfC
17 16 adantr φfACBCfCBf=CfC
18 14 17 jca φfACBCfCBfCBf=CfC
19 fsn2g CZf:CBfCBf=CfC
20 3 19 syl φf:CBfCBf=CfC
21 20 ad2antrr φfACBCfCBf:CBfCBf=CfC
22 18 21 mpbird φfACBCfCBf:CB
23 2 ad2antrr φfACBCfCBBW
24 snex CV
25 24 a1i φfACBCfCBCV
26 23 25 elmapd φfACBCfCBfBCf:CB
27 22 26 mpbird φfACBCfCBfBC
28 eldifn fACBC¬fBC
29 28 ad2antlr φfACBCfCB¬fBC
30 27 29 pm2.65da φfACBC¬fCB
31 13 30 eldifd φfACBCfCAB
32 31 16 jca φfACBCfCABf=CfC
33 fsn2g CZf:CABfCABf=CfC
34 3 33 syl φf:CABfCABf=CfC
35 34 adantr φfACBCf:CABfCABf=CfC
36 32 35 mpbird φfACBCf:CAB
37 difssd φABA
38 1 37 ssexd φABV
39 24 a1i φCV
40 38 39 elmapd φfABCf:CAB
41 40 adantr φfACBCfABCf:CAB
42 36 41 mpbird φfACBCfABC
43 42 ralrimiva φfACBCfABC
44 dfss3 ACBCABCfACBCfABC
45 43 44 sylibr φACBCABC
46 3 snn0d φC
47 1 2 39 46 difmap φABCACBC
48 45 47 eqssd φACBC=ABC