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

Theorem disjsn 3432
 Description: Intersection with the singleton of a non-member is disjoint. (Contributed by NM, 22-May-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by Wolf Lammen, 30-Sep-2014.)
Assertion
Ref Expression
disjsn ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)

Proof of Theorem disjsn
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 disj1 3270 . 2 ((𝐴 ∩ {𝐵}) = ∅ ↔ ∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}))
2 con2b 593 . . . 4 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ (𝑥 ∈ {𝐵} → ¬ 𝑥𝐴))
3 velsn 3392 . . . . 5 (𝑥 ∈ {𝐵} ↔ 𝑥 = 𝐵)
43imbi1i 227 . . . 4 ((𝑥 ∈ {𝐵} → ¬ 𝑥𝐴) ↔ (𝑥 = 𝐵 → ¬ 𝑥𝐴))
5 imnan 624 . . . 4 ((𝑥 = 𝐵 → ¬ 𝑥𝐴) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
62, 4, 53bitri 195 . . 3 ((𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ¬ (𝑥 = 𝐵𝑥𝐴))
76albii 1359 . 2 (∀𝑥(𝑥𝐴 → ¬ 𝑥 ∈ {𝐵}) ↔ ∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴))
8 alnex 1388 . . 3 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
9 df-clel 2036 . . 3 (𝐵𝐴 ↔ ∃𝑥(𝑥 = 𝐵𝑥𝐴))
108, 9xchbinxr 608 . 2 (∀𝑥 ¬ (𝑥 = 𝐵𝑥𝐴) ↔ ¬ 𝐵𝐴)
111, 7, 103bitri 195 1 ((𝐴 ∩ {𝐵}) = ∅ ↔ ¬ 𝐵𝐴)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98  ∀wal 1241   = wceq 1243  ∃wex 1381   ∈ wcel 1393   ∩ cin 2916  ∅c0 3224  {csn 3375 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 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-fal 1249  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559  df-dif 2920  df-in 2924  df-nul 3225  df-sn 3381 This theorem is referenced by:  disjsn2  3433  orddisj  4270  ndmima  4702  funtpg  4950  fnunsn  5006  ressnop0  5344  ftpg  5347  fsnunf  5362  fsnunfv  5363  phpm  6327  fiunsnnn  6338  ac6sfi  6352  fzpreddisj  8933  fzp1disj  8942  frecfzennn  9203
 Copyright terms: Public domain W3C validator