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 634	. . . 4 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
2		eldif 3443	. . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	2	bibi2i 314	. . . 4 |- ( ( x e. A <-> x e. ( A \ B ) ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
4	1, 3	bitr4i 255	. . 3 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> x e. ( A \ B ) ) )
5	4	albii 1687	. 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 2413	. 2 |- ( A = ( A \ B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
8	5, 6, 7	3bitr4i 280	1 |- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   e. wcel 1867   \ cdif 3430   i^i cin 3432   (/)c0 3758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-v 3080  df-dif 3436  df-in 3440  df-nul 3759

This theorem is referenced by:  disjel  3836  disj4  3838  uneqdifeq  3881  difprsn1  4130  diftpsn3  4132  ssunsn2  4153  orddif  5526  php  7753  hartogslem1  8048  infeq5i  8132  cantnfp1lem3  8175  cda1dif  8595  infcda1  8612  ssxr  9692  dprd2da  17603  dmdprdsplit2lem  17606  ablfac1eulem  17633  lbsextlem4  18312  opsrtoslem2  18636  alexsublem  20983  volun  22392  lhop1lem  22859  ex-dif  25744  difeq  28013  imadifxp  28077  disjdsct  28149  carsgclctunlem1  29004  probun  29104  ballotlemfp1  29176  topdifinfeq  31513  finixpnum  31663  poimirlem11  31684  poimirlem12  31685  poimirlem13  31686  poimirlem14  31687  poimirlem16  31689  poimirlem18  31691  poimirlem21  31694  poimirlem22  31695  poimirlem27  31700  asindmre  31760  kelac2  35662  pwfi2f1o  35693  iccdifioo  37234  iccdifprioo  37235