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.

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 3333	. . . . 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 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 ) ) )
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 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