Theorem disjsn 2502

Description: Intersection with the singleton of a non-member is disjoint.

Assertion

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

Proof of Theorem disjsn

Step	Hyp	Ref	Expression
1		noel 2336	. . . 4 |- -. B e. (/)
2		eleq2 1578	. . . 4 |- ((A i^i {B}) = (/) -> (B e. (A i^i {B}) <-> B e. (/)))
3	1, 2	mtbiri 722	. . 3 |- ((A i^i {B}) = (/) -> -. B e. (A i^i {B}))
4		snidg 2494	. . . . 5 |- (B e. A -> B e. {B})
5	4	ancli 294	. . . 4 |- (B e. A -> (B e. A /\ B e. {B}))
6		elin 2259	. . . 4 |- (B e. (A i^i {B}) <-> (B e. A /\ B e. {B}))
7	5, 6	sylibr 198	. . 3 |- (B e. A -> B e. (A i^i {B}))
8	3, 7	nsyl 115	. 2 |- ((A i^i {B}) = (/) -> -. B e. A)
9		eleq1 1577	. . . . . . . 8 |- (x = B -> (x e. A <-> B e. A))
10	9	biimpcd 153	. . . . . . 7 |- (x e. A -> (x = B -> B e. A))
11		elsn 2479	. . . . . . 7 |- (x e. {B} <-> x = B)
12	10, 11	syl5ib 204	. . . . . 6 |- (x e. A -> (x e. {B} -> B e. A))
13	12	con3d 95	. . . . 5 |- (x e. A -> (-. B e. A -> -. x e. {B}))
14	13	com12 11	. . . 4 |- (-. B e. A -> (x e. A -> -. x e. {B}))
15	14	19.21aiv 1324	. . 3 |- (-. B e. A -> A.x(x e. A -> -. x e. {B}))
16		disj1 2365	. . 3 |- ((A i^i {B}) = (/) <-> A.x(x e. A -> -. x e. {B}))
17	15, 16	sylibr 198	. 2 |- (-. B e. A -> (A i^i {B}) = (/))
18	8, 17	impbii 155	1 |- ((A i^i {B}) = (/) <-> -. B e. A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   /\ wa 221  A.wal 990   = wceq 992   e. wcel 994   i^i cin 2098  (/)c0 2332  {csn 2467

This theorem is referenced by:  disjsn2 2503  orddisj 3013  ndmima 3526  dmsnn0 3573  ac6sfilem3 4590  limensuci 4653  php 4660  pm54.43 4715  infensuc 4784  kmlem2 4912  unsnen 4983  renfdisj 5693  cnconst 7990  sncld 7997  subtopsin2 11067  reconnlem1 11507  locfincomp 11575  locfindsc 11576  ist1-2 11603

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-ral 1695  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-nul 2333  df-sn 2470  df-pr 2471

Copyright terms: Public domain