Theorem disjsn 3656

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 3475	. 2 |- ( ( A i^i { B } ) = (/) <-> A. x ( x e. A -> -. x e. { B } ) )
2		con2b 669	. . . 4 |- ( ( x e. A -> -. x e. { B } ) <-> ( x e. { B } -> -. x e. A ) )
3		velsn 3611	. . . . 5 |- ( x e. { B } <-> x = B )
4	3	imbi1i 238	. . . 4 |- ( ( x e. { B } -> -. x e. A ) <-> ( x = B -> -. x e. A ) )
5		imnan 690	. . . 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 1470	. 2 |- ( A. x ( x e. A -> -. x e. { B } ) <-> A. x -. ( x = B /\ x e. A ) )
8		alnex 1499	. . 3 |- ( A. x -. ( x = B /\ x e. A ) <-> -. E. x ( x = B /\ x e. A ) )
9		df-clel 2173	. . 3 |- ( B e. A <-> E. x ( x = B /\ x e. A ) )
10	8, 9	xchbinxr 683	. 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 1351   = wceq 1353   E.wex 1492   e. wcel 2148   i^i cin 3130   (/)c0 3424   {csn 3594

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2741  df-dif 3133  df-in 3137  df-nul 3425  df-sn 3600

This theorem is referenced by:  disjsn2  3657  ssdifsn  3722  orddisj  4547  ndmima  5007  funtpg  5269  fnunsn  5325  ressnop0  5700  ftpg  5703  fsnunf  5719  fsnunfv  5720  enpr2d  6820  phpm  6868  fiunsnnn  6884  ac6sfi  6901  unsnfi  6921  tpfidisj  6930  iunfidisj  6948  pm54.43  7192  dju1en  7215  fzpreddisj  10074  fzp1disj  10083  frecfzennn  10429  hashunsng  10790  hashxp  10809  fsumsplitsn  11421  sumtp  11425  fsumsplitsnun  11430  fsum2dlemstep  11445  fsumconst  11465  fsumabs  11476  fsumiun  11488  fprodm1  11609  fprodunsn  11615  fprod2dlemstep  11633  fprodsplitsn  11644  ennnfonelemhf1o  12417  structcnvcnv  12481  fsumcncntop  14217