Theorem disj3 3834

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.

Step	Hyp	Ref	Expression
1		pm4.71 630	. . . 4 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
2		eldif 3449	. . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	2	bibi2i 313	. . . 4 |- ( ( x e. A <-> x e. ( A \ B ) ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
4	1, 3	bitr4i 252	. . 3 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> x e. ( A \ B ) ) )
5	4	albii 1611	. 2 |- ( A. x ( x e. A -> -. x e. B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
6		disj1 3832	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
7		dfcleq 2447	. 2 |- ( A = ( A \ B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
8	5, 6, 7	3bitr4i 277	1 |- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1368   = wceq 1370   e. wcel 1758   \ cdif 3436   i^i cin 3438   (/)c0 3748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-dif 3442  df-in 3446  df-nul 3749

This theorem is referenced by:  disjel  3836  disj4  3838  uneqdifeq  3878  difprsn1  4121  diftpsn3  4123  ssunsn2  4143  orddif  4923  php  7608  hartogslem1  7870  infeq5i  7956  cantnfp1lem3  8002  cantnfp1lem3OLD  8028  cda1dif  8459  infcda1  8476  ssxr  9558  dprd2da  16666  dmdprdsplit2lem  16669  ablfac1eulem  16698  lbsextlem4  17368  opsrtoslem2  17693  alexsublem  19751  volun  21162  lhop1lem  21621  ex-dif  23802  difeq  26071  imadifxp  26110  disjdsct  26169  probun  26966  ballotlemfp1  27038  finixpnum  28582  asindmre  28647  kelac2  29586  pwfi2f1o  29619