MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disj Structured version   Unicode version

Theorem disj 3660
Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)
Assertion
Ref Expression
disj  |-  ( ( A  i^i  B )  =  (/)  <->  A. x  e.  A  -.  x  e.  B
)
Distinct variable groups:    x, A    x, B

Proof of Theorem disj
StepHypRef Expression
1 df-in 3319 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
21eqeq1i 2442 . . 3  |-  ( ( A  i^i  B )  =  (/)  <->  { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/) )
3 abeq1 2541 . . 3  |-  ( { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/)  <->  A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
4 imnan 412 . . . . 5  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  -.  ( x  e.  A  /\  x  e.  B ) )
5 noel 3624 . . . . . 6  |-  -.  x  e.  (/)
65nbn 337 . . . . 5  |-  ( -.  ( x  e.  A  /\  x  e.  B
)  <->  ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
74, 6bitr2i 242 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  <->  x  e.  (/) )  <->  ( x  e.  A  ->  -.  x  e.  B ) )
87albii 1575 . . 3  |-  ( A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) )  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
92, 3, 83bitri 263 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
10 df-ral 2702 . 2  |-  ( A. x  e.  A  -.  x  e.  B  <->  A. x
( x  e.  A  ->  -.  x  e.  B
) )
119, 10bitr4i 244 1  |-  ( ( A  i^i  B )  =  (/)  <->  A. x  e.  A  -.  x  e.  B
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725   {cab 2421   A.wral 2697    i^i cin 3311   (/)c0 3620
This theorem is referenced by:  disjr  3661  disj1  3662  disjne  3665  onint  4767  onxpdisj  4949  zfreg  7553  kmlem4  8023  fin23lem30  8212  fin23lem31  8213  isf32lem3  8225  fpwwe2  8508  renfdisj  9128  injresinjlem  11189  metdsge  18869  spthispth  21563  subfacp1lem1  24855  dfpo2  25368  stoweidlem26  27706  stoweidlem59  27739  otiunsndisj  28020  otiunsndisjX  28021  2spotdisj  28351  2spotiundisj  28352  2spotmdisj  28358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-dif 3315  df-in 3319  df-nul 3621
  Copyright terms: Public domain W3C validator