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

Theorem disj 3495
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 3159 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
21eqeq1i 2290 . . 3  |-  ( ( A  i^i  B )  =  (/)  <->  { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/) )
3 abeq1 2389 . . 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 3459 . . . . . 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 1553 . . 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 2548 . 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 1527    = wceq 1623    e. wcel 1684   {cab 2269   A.wral 2543    i^i cin 3151   (/)c0 3455
This theorem is referenced by:  disjr  3496  disj1  3497  disjne  3500  onint  4586  onxpdisj  4769  zfreg  7309  kmlem4  7779  fin23lem30  7968  fin23lem31  7969  isf32lem3  7981  fpwwe2  8265  renfdisj  8885  metdsge  18353  subfacp1lem1  23710  dfpo2  24112  funpartfv  24483  imfstnrelc  25081  inttpemp  25139  bsstrs  26146  nbssntrs  26147  stoweidlem26  27775  stoweidlem59  27808
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-dif 3155  df-in 3159  df-nul 3456
  Copyright terms: Public domain W3C validator