Theorem disjsn 3089

Description: Intersection with the singleton of a non-member is disjoint. (The proof was shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
disjsn	|- ((A i^i {B}) = (/) <-> -. B e. A)

Proof of Theorem disjsn

Step	Hyp	Ref	Expression
1		con2b 182	. . . . 5 |- ((x e. A -> -. x e. {B}) <-> (x e. {B} -> -. x e. A))
2		elsn 3058	. . . . . 6 |- (x e. {B} <-> x = B)
3	2	imbi1i 203	. . . . 5 |- ((x e. {B} -> -. x e. A) <-> (x = B -> -. x e. A))
4		imnan 261	. . . . 5 |- ((x = B -> -. x e. A) <-> -. (x = B /\ x e. A))
5	1, 3, 4	3bitri 194	. . . 4 |- ((x e. A -> -. x e. {B}) <-> -. (x = B /\ x e. A))
6	5	albii 1346	. . 3 |- (A.x(x e. A -> -. x e. {B}) <-> A.x -. (x = B /\ x e. A))
7		alnex 1380	. . 3 |- (A.x -. (x = B /\ x e. A) <-> -. E.x(x = B /\ x e. A))
8	6, 7	bitri 190	. 2 |- (A.x(x e. A -> -. x e. {B}) <-> -. E.x(x = B /\ x e. A))
9		disj1 2915	. 2 |- ((A i^i {B}) = (/) <-> A.x(x e. A -> -. x e. {B}))
10		df-clel 1880	. . 3 |- (B e. A <-> E.x(x = B /\ x e. A))
11	10	notbii 204	. 2 |- (-. B e. A <-> -. E.x(x = B /\ x e. A))
12	8, 9, 11	3bitr4i 200	1 |- ((A i^i {B}) = (/) <-> -. B e. A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   i^i cin 2592  (/)c0 2875  {csn 3044

This theorem is referenced by:  disjsn2 3091  orddisj 3701  ndmima 4300  dmsnn0OLD 4363  ac6sfilem3 5508  limensuci 5600  php 5607  pm54.43 5662  infensuc 5745  kmlem2 5928  unsnen 5985  renfdisjOLD 6713  ssxr 6714  cnconst 9057  sncld 9064  bnj1421 13532  isprm2lem 13774  wfrlem13 13969  subtopsin2 14907  reconnlem1 15446  locfincomp 15514  locfindsc 15515  ist1-2 15542

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-v 2294  df-dif 2597  df-in 2603  df-nul 2876  df-sn 3049

Copyright terms: Public domain