ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  diftpsn3 Structured version   GIF version

Theorem diftpsn3 3479
Description: Removal of a singleton from an unordered triple. (Contributed by Alexander van der Vekens, 5-Oct-2017.)
Assertion
Ref Expression
diftpsn3 ((A𝐶 B𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A, B})

Proof of Theorem diftpsn3
StepHypRef Expression
1 df-tp 3358 . . . 4 {A, B, 𝐶} = ({A, B} ∪ {𝐶})
21a1i 9 . . 3 ((A𝐶 B𝐶) → {A, B, 𝐶} = ({A, B} ∪ {𝐶}))
32difeq1d 3038 . 2 ((A𝐶 B𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = (({A, B} ∪ {𝐶}) ∖ {𝐶}))
4 difundir 3167 . . 3 (({A, B} ∪ {𝐶}) ∖ {𝐶}) = (({A, B} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶}))
54a1i 9 . 2 ((A𝐶 B𝐶) → (({A, B} ∪ {𝐶}) ∖ {𝐶}) = (({A, B} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})))
6 df-pr 3357 . . . . . . . . 9 {A, B} = ({A} ∪ {B})
76a1i 9 . . . . . . . 8 ((A𝐶 B𝐶) → {A, B} = ({A} ∪ {B}))
87ineq1d 3114 . . . . . . 7 ((A𝐶 B𝐶) → ({A, B} ∩ {𝐶}) = (({A} ∪ {B}) ∩ {𝐶}))
9 incom 3106 . . . . . . . . 9 (({A} ∪ {B}) ∩ {𝐶}) = ({𝐶} ∩ ({A} ∪ {B}))
10 indi 3161 . . . . . . . . 9 ({𝐶} ∩ ({A} ∪ {B})) = (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B}))
119, 10eqtri 2042 . . . . . . . 8 (({A} ∪ {B}) ∩ {𝐶}) = (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B}))
1211a1i 9 . . . . . . 7 ((A𝐶 B𝐶) → (({A} ∪ {B}) ∩ {𝐶}) = (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})))
13 necom 2267 . . . . . . . . . . 11 (A𝐶𝐶A)
14 disjsn2 3407 . . . . . . . . . . 11 (𝐶A → ({𝐶} ∩ {A}) = ∅)
1513, 14sylbi 114 . . . . . . . . . 10 (A𝐶 → ({𝐶} ∩ {A}) = ∅)
1615adantr 261 . . . . . . . . 9 ((A𝐶 B𝐶) → ({𝐶} ∩ {A}) = ∅)
17 necom 2267 . . . . . . . . . . 11 (B𝐶𝐶B)
18 disjsn2 3407 . . . . . . . . . . 11 (𝐶B → ({𝐶} ∩ {B}) = ∅)
1917, 18sylbi 114 . . . . . . . . . 10 (B𝐶 → ({𝐶} ∩ {B}) = ∅)
2019adantl 262 . . . . . . . . 9 ((A𝐶 B𝐶) → ({𝐶} ∩ {B}) = ∅)
2116, 20uneq12d 3075 . . . . . . . 8 ((A𝐶 B𝐶) → (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) = (∅ ∪ ∅))
22 unidm 3063 . . . . . . . 8 (∅ ∪ ∅) = ∅
2321, 22syl6eq 2070 . . . . . . 7 ((A𝐶 B𝐶) → (({𝐶} ∩ {A}) ∪ ({𝐶} ∩ {B})) = ∅)
248, 12, 233eqtrd 2058 . . . . . 6 ((A𝐶 B𝐶) → ({A, B} ∩ {𝐶}) = ∅)
25 disj3 3249 . . . . . 6 (({A, B} ∩ {𝐶}) = ∅ ↔ {A, B} = ({A, B} ∖ {𝐶}))
2624, 25sylib 127 . . . . 5 ((A𝐶 B𝐶) → {A, B} = ({A, B} ∖ {𝐶}))
2726eqcomd 2027 . . . 4 ((A𝐶 B𝐶) → ({A, B} ∖ {𝐶}) = {A, B})
28 difid 3269 . . . . 5 ({𝐶} ∖ {𝐶}) = ∅
2928a1i 9 . . . 4 ((A𝐶 B𝐶) → ({𝐶} ∖ {𝐶}) = ∅)
3027, 29uneq12d 3075 . . 3 ((A𝐶 B𝐶) → (({A, B} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = ({A, B} ∪ ∅))
31 un0 3228 . . 3 ({A, B} ∪ ∅) = {A, B}
3230, 31syl6eq 2070 . 2 ((A𝐶 B𝐶) → (({A, B} ∖ {𝐶}) ∪ ({𝐶} ∖ {𝐶})) = {A, B})
333, 5, 323eqtrd 2058 1 ((A𝐶 B𝐶) → ({A, B, 𝐶} ∖ {𝐶}) = {A, B})
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1228  wne 2186  cdif 2891  cun 2892  cin 2893  c0 3201  {csn 3350  {cpr 3351  {ctp 3352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rab 2293  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-sn 3356  df-pr 3357  df-tp 3358
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator