Theorem disjsn 3705

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	|- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Proof of Theorem disjsn

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		disj1 3519	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 671	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3660	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 238	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 692	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 206	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1494	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1523	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2203	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 685	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 206	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1371   = wceq 1373   E.wex 1516   e. wcel 2178   i^i cin 3173   (/)c0 3468   {csn 3643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-v 2778  df-dif 3176  df-in 3180  df-nul 3469  df-sn 3649

This theorem is referenced by:  disjsn2  3706  ssdifsn  3772  opwo0id  4311  orddisj  4612  ndmima  5078  funtpg  5344  fnunsn  5402  ressnop0  5788  ftpg  5791  fsnunf  5807  fsnunfv  5808  enpr2d  6935  phpm  6988  fiunsnnn  7004  ac6sfi  7021  unsnfi  7042  tpfidisj  7052  iunfidisj  7074  pm54.43  7324  dju1en  7356  fzpreddisj  10228  fzp1disj  10237  frecfzennn  10608  hashunsng  10989  hashxp  11008  fsumsplitsn  11836  sumtp  11840  fsumsplitsnun  11845  fsum2dlemstep  11860  fsumconst  11880  fsumabs  11891  fsumiun  11903  fprodm1  12024  fprodunsn  12030  fprod2dlemstep  12048  fprodsplitsn  12059  bitsinv1  12388  ennnfonelemhf1o  12899  structcnvcnv  12963  fsumcncntop  15154  dvmptfsum  15312  perfectlem2  15587