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

Theorem disj3 3672
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 612 . . . 4  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  <->  ( x  e.  A  /\  -.  x  e.  B ) ) )
2 eldif 3330 . . . . 5  |-  ( x  e.  ( A  \  B )  <->  ( x  e.  A  /\  -.  x  e.  B ) )
32bibi2i 305 . . . 4  |-  ( ( x  e.  A  <->  x  e.  ( A  \  B ) )  <->  ( x  e.  A  <->  ( x  e.  A  /\  -.  x  e.  B ) ) )
41, 3bitr4i 244 . . 3  |-  ( ( x  e.  A  ->  -.  x  e.  B
)  <->  ( x  e.  A  <->  x  e.  ( A  \  B ) ) )
54albii 1575 . 2  |-  ( A. x ( x  e.  A  ->  -.  x  e.  B )  <->  A. x
( x  e.  A  <->  x  e.  ( A  \  B ) ) )
6 disj1 3670 . 2  |-  ( ( A  i^i  B )  =  (/)  <->  A. x ( x  e.  A  ->  -.  x  e.  B )
)
7 dfcleq 2430 . 2  |-  ( A  =  ( A  \  B )  <->  A. x
( x  e.  A  <->  x  e.  ( A  \  B ) ) )
85, 6, 73bitr4i 269 1  |-  ( ( A  i^i  B )  =  (/)  <->  A  =  ( A  \  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    \ cdif 3317    i^i cin 3319   (/)c0 3628
This theorem is referenced by:  disjel  3674  disj4  3676  uneqdifeq  3716  difprsn1  3935  diftpsn3  3937  ssunsn2  3958  orddif  4675  php  7291  hartogslem1  7511  infeq5i  7591  cantnfp1lem3  7636  cda1dif  8056  infcda1  8073  ssxr  9145  dprd2da  15600  dmdprdsplit2lem  15603  ablfac1eulem  15630  lbsextlem4  16233  opsrtoslem2  16545  alexsublem  18075  volun  19439  lhop1lem  19897  ex-dif  21731  difeq  23998  imadifxp  24038  disjdsct  24090  probun  24677  ballotlemfp1  24749  kelac2  27140  pwfi2f1o  27237
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958  df-dif 3323  df-in 3327  df-nul 3629
  Copyright terms: Public domain W3C validator