Theorem disjsn 3645

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 3465	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 664	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3600	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 237	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 685	. . . 4 |- ( ( x = B -> -. x e. A ) <-> -. ( x = B /\ x e. A ) )
6	2, 4, 5	3bitri 205	. . 3 |- ( ( x e. A -> -. x e. { B } ) <-> -. ( x = B /\ x e. A ) )
7	6	albii 1463	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1492	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2166	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 678	. 2 |- ( A. x -. ( x = B /\ x e. A ) <-> -. B e. A )
11	1, 7, 10	3bitri 205	1 |- ( ( A i^i { B } ) = (/) <-> -. B e. A )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   A.wal 1346   = wceq 1348   E.wex 1485   e. wcel 2141   i^i cin 3120   (/)c0 3414   {csn 3583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-v 2732  df-dif 3123  df-in 3127  df-nul 3415  df-sn 3589

This theorem is referenced by:  disjsn2  3646  ssdifsn  3711  orddisj  4530  ndmima  4988  funtpg  5249  fnunsn  5305  ressnop0  5677  ftpg  5680  fsnunf  5696  fsnunfv  5697  enpr2d  6795  phpm  6843  fiunsnnn  6859  ac6sfi  6876  unsnfi  6896  tpfidisj  6905  iunfidisj  6923  pm54.43  7167  dju1en  7190  fzpreddisj  10027  fzp1disj  10036  frecfzennn  10382  hashunsng  10742  hashxp  10761  fsumsplitsn  11373  sumtp  11377  fsumsplitsnun  11382  fsum2dlemstep  11397  fsumconst  11417  fsumabs  11428  fsumiun  11440  fprodm1  11561  fprodunsn  11567  fprod2dlemstep  11585  fprodsplitsn  11596  ennnfonelemhf1o  12368  structcnvcnv  12432  fsumcncntop  13350