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

Theorem disj 3816
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 3422 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
21eqeq1i 2466 . . 3  |-  ( ( A  i^i  B )  =  (/)  <->  { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/) )
3 abeq1 2571 . . 3  |-  ( { x  |  ( x  e.  A  /\  x  e.  B ) }  =  (/)  <->  A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
4 imnan 428 . . . . 5  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  -.  ( x  e.  A  /\  x  e.  B ) )
5 noel 3746 . . . . . 6  |-  -.  x  e.  (/)
65nbn 353 . . . . 5  |-  ( -.  ( x  e.  A  /\  x  e.  B
)  <->  ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) ) )
74, 6bitr2i 258 . . . 4  |-  ( ( ( x  e.  A  /\  x  e.  B
)  <->  x  e.  (/) )  <->  ( x  e.  A  ->  -.  x  e.  B ) )
87albii 1701 . . 3  |-  ( A. x ( ( x  e.  A  /\  x  e.  B )  <->  x  e.  (/) )  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
92, 3, 83bitri 279 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
10 df-ral 2753 . 2  |-  ( A. x  e.  A  -.  x  e.  B  <->  A. x
( x  e.  A  ->  -.  x  e.  B
) )
119, 10bitr4i 260 1  |-  ( ( A  i^i  B )  =  (/)  <->  A. x  e.  A  -.  x  e.  B
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1452    = wceq 1454    e. wcel 1897   {cab 2447   A.wral 2748    i^i cin 3414   (/)c0 3742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-v 3058  df-dif 3418  df-in 3422  df-nul 3743
This theorem is referenced by:  disjr  3817  disj1  3818  disjne  3821  otiunsndisj  4720  onxpdisj  5560  f0rn0  5790  onint  6648  zfreg  8135  kmlem4  8608  fin23lem30  8797  fin23lem31  8798  isf32lem3  8810  fpwwe2  9093  renfdisj  9719  fvinim0ffz  12054  metdsge  21914  metdsgeOLD  21929  spthispth  25351  2spotdisj  25837  2spotiundisj  25838  2spotmdisj  25844  subfacp1lem1  29950  dfpo2  30443  dvmptfprodlem  37856  stoweidlem26  37923  stoweidlem59  37957  iundjiunlem  38334  otiunsndisjX  39045
  Copyright terms: Public domain W3C validator