Theorem disjsn 3654

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 3473	. 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 3609	. . . . 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 3128   (/)c0 3422   {csn 3592

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 2739  df-dif 3131  df-in 3135  df-nul 3423  df-sn 3598

This theorem is referenced by:  disjsn2  3655  ssdifsn  3720  orddisj  4545  ndmima  5005  funtpg  5267  fnunsn  5323  ressnop0  5697  ftpg  5700  fsnunf  5716  fsnunfv  5717  enpr2d  6816  phpm  6864  fiunsnnn  6880  ac6sfi  6897  unsnfi  6917  tpfidisj  6926  iunfidisj  6944  pm54.43  7188  dju1en  7211  fzpreddisj  10070  fzp1disj  10079  frecfzennn  10425  hashunsng  10786  hashxp  10805  fsumsplitsn  11417  sumtp  11421  fsumsplitsnun  11426  fsum2dlemstep  11441  fsumconst  11461  fsumabs  11472  fsumiun  11484  fprodm1  11605  fprodunsn  11611  fprod2dlemstep  11629  fprodsplitsn  11640  ennnfonelemhf1o  12413  structcnvcnv  12477  fsumcncntop  14026