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

Theorem disj3 3718
Description: Two ways of saying that two classes are disjoint. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
disj3  |-  ( ( A  i^i  B )  =  (/)  <->  A  =  ( A  \  B ) )

Proof of Theorem disj3
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 pm4.71 630 . . . 4  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  <->  ( x  e.  A  /\  -.  x  e.  B ) ) )
2 eldif 3333 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32bibi2i 313 . . . 4  |-  ( ( x  e.  A  <->  x  e.  ( A  \  B ) )  <->  ( x  e.  A  <->  ( x  e.  A  /\  -.  x  e.  B ) ) )
41, 3bitr4i 252 . . 3  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  <->  x  e.  ( A  \  B ) ) )
54albii 1610 . 2  |-  ( A. x ( x  e.  A  ->  -.  x  e.  B )  <->  A. x
( x  e.  A  <->  x  e.  ( A  \  B ) ) )
6 disj1 3716 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
7 dfcleq 2432 . 2  |-  ( A  =  ( A  \  B )  <->  A. x
( x  e.  A  <->  x  e.  ( A  \  B ) ) )
85, 6, 73bitr4i 277 1  |-  ( ( A  i^i  B )  =  (/)  <->  A  =  ( A  \  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756    \ cdif 3320    i^i cin 3322   (/)c0 3632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969  df-dif 3326  df-in 3330  df-nul 3633
This theorem is referenced by:  disjel  3720  disj4  3722  uneqdifeq  3762  difprsn1  4005  diftpsn3  4007  ssunsn2  4027  orddif  4807  php  7487  hartogslem1  7748  infeq5i  7834  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  cda1dif  8337  infcda1  8354  ssxr  9436  dprd2da  16529  dmdprdsplit2lem  16532  ablfac1eulem  16561  lbsextlem4  17219  opsrtoslem2  17541  alexsublem  19591  volun  21001  lhop1lem  21460  ex-dif  23581  difeq  25850  imadifxp  25890  disjdsct  25949  probun  26754  ballotlemfp1  26826  finixpnum  28367  asindmre  28432  kelac2  29371  pwfi2f1o  29404
  Copyright terms: Public domain W3C validator