Theorem disjsn 3735

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 3547	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 675	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3690	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 238	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 697	. . . 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 1519	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1548	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2227	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 690	. 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 1396   = wceq 1398   E.wex 1541   e. wcel 2202   i^i cin 3200   (/)c0 3496   {csn 3673

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-v 2805  df-dif 3203  df-in 3207  df-nul 3497  df-sn 3679

This theorem is referenced by:  disjsn2  3736  ssdifsn  3805  opwo0id  4347  orddisj  4650  ndmima  5120  funtpg  5388  fnunsn  5446  ressnop0  5843  ftpg  5846  fsnunf  5862  fsnunfv  5863  enpr2d  7040  phpm  7095  fiunsnnn  7113  ac6sfi  7130  unsnfi  7154  tpfidisj  7164  iunfidisj  7188  pm54.43  7455  dju1en  7488  fzpreddisj  10368  fzp1disj  10377  frecfzennn  10751  hashunsng  11134  hashxp  11153  fsumsplitsn  12051  sumtp  12055  fsumsplitsnun  12060  fsum2dlemstep  12075  fsumconst  12095  fsumabs  12106  fsumiun  12118  fprodm1  12239  fprodunsn  12245  fprod2dlemstep  12263  fprodsplitsn  12274  bitsinv1  12603  ennnfonelemhf1o  13114  structcnvcnv  13178  fsumcncntop  15378  dvmptfsum  15536  perfectlem2  15814  p1evtxdeqfilem  16252  trlsegvdegfi  16408  gfsump1  16815