Theorem disjsn2 3730

Description: Intersection of distinct singletons is disjoint. (Contributed by NM, 25-May-1998.)

Assertion

Ref	Expression
disjsn2	|- ( A =/= B -> ( { A } i^i { B } ) = (/) )

Proof of Theorem disjsn2

Step	Hyp	Ref	Expression
1		elsni 3685	. . . 4 |- ( B e. { A } -> B = A )
2	1	eqcomd 2235	. . 3 |- ( B e. { A } -> A = B )
3	2	necon3ai 2449	. 2 |- ( A =/= B -> -. B e. { A } )
4		disjsn 3729	. 2 |- ( ( { A } i^i { B } ) = (/) <-> -. B e. { A } )
5	3, 4	sylibr 134	1 |- ( A =/= B -> ( { A } i^i { B } ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   e. wcel 2200   =/= wne 2400   i^i cin 3197   (/)c0 3492   {csn 3667

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-v 2802  df-dif 3200  df-in 3204  df-nul 3493  df-sn 3673

This theorem is referenced by:  disjpr2  3731  difprsn1  3810  diftpsn3  3812  xpsndisj  5161  funprg  5377  funtp  5380  f1oprg  5625  xp01disjl  6597  enpr2d  6992  phplem1  7033  prfidisj  7112  djuinr  7253  pm54.43  7386  pr2nelem  7387  sumpr  11964  setsfun0  13108  setscom  13112  perfectlem2  15714