Theorem disj3 3871

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 3486	. . . . 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 1620	. 2 |- ( A. x ( x e. A -> -. x e. B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
6		disj1 3869	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
7		dfcleq 2460	. 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 1377   = wceq 1379   e. wcel 1767   \ cdif 3473   i^i cin 3475   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-dif 3479  df-in 3483  df-nul 3786

This theorem is referenced by:  disjel  3873  disj4  3875  uneqdifeq  3915  difprsn1  4163  diftpsn3  4165  ssunsn2  4186  orddif  4971  php  7701  hartogslem1  7966  infeq5i  8052  cantnfp1lem3  8098  cantnfp1lem3OLD  8124  cda1dif  8555  infcda1  8572  ssxr  9653  dprd2da  16890  dmdprdsplit2lem  16893  ablfac1eulem  16922  lbsextlem4  17602  opsrtoslem2  17936  alexsublem  20295  volun  21706  lhop1lem  22165  ex-dif  24837  difeq  27106  imadifxp  27147  disjdsct  27209  probun  28014  ballotlemfp1  28086  finixpnum  29631  asindmre  29695  kelac2  30631  pwfi2f1o  30664  iccdifioo  31135  iccdifprioo  31136