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

Theorem disj 3508
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 3172 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
21eqeq1i 2303 . . 3  |-  ( ( A  i^i  B )  =  (/)  <->  { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/) )
3 abeq1 2402 . . 3  |-  ( { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/)  <->  A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
4 imnan 411 . . . . 5  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  -.  ( x  e.  A  /\  x  e.  B ) )
5 noel 3472 . . . . . 6  |-  -.  x  e.  (/)
65nbn 336 . . . . 5  |-  ( -.  ( x  e.  A  /\  x  e.  B
)  <->  ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
74, 6bitr2i 241 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  <->  x  e.  (/) )  <->  ( x  e.  A  ->  -.  x  e.  B ) )
87albii 1556 . . 3  |-  ( A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) )  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
92, 3, 83bitri 262 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
10 df-ral 2561 . 2  |-  ( A. x  e.  A  -.  x  e.  B  <->  A. x
( x  e.  A  ->  -.  x  e.  B
) )
119, 10bitr4i 243 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 176    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556    i^i cin 3164   (/)c0 3468
This theorem is referenced by:  disjr  3509  disj1  3510  disjne  3513  onint  4602  onxpdisj  4785  zfreg  7325  kmlem4  7795  fin23lem30  7984  fin23lem31  7985  isf32lem3  7997  fpwwe2  8281  renfdisj  8901  metdsge  18369  subfacp1lem1  23725  dfpo2  24183  imfstnrelc  25184  inttpemp  25242  bsstrs  26249  nbssntrs  26250  stoweidlem26  27878  stoweidlem59  27911  injresinjlem  28214  spthispth  28359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-dif 3168  df-in 3172  df-nul 3469
  Copyright terms: Public domain W3C validator