Theorem disj3 4021

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 662	. . . 4 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
2		eldif 3584	. . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	2	bibi2i 327	. . . 4 |- ( ( x e. A <-> x e. ( A \ B ) ) <-> ( x e. A <-> ( x e. A /\ -. x e. B ) ) )
4	1, 3	bitr4i 267	. . 3 |- ( ( x e. A -> -. x e. B ) <-> ( x e. A <-> x e. ( A \ B ) ) )
5	4	albii 1747	. 2 |- ( A. x ( x e. A -> -. x e. B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
6		disj1 4019	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
7		dfcleq 2616	. 2 |- ( A = ( A \ B ) <-> A. x ( x e. A <-> x e. ( A \ B ) ) )
8	5, 6, 7	3bitr4i 292	1 |- ( ( A i^i B ) = (/) <-> A = ( A \ B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   \ cdif 3571   i^i cin 3573   (/)c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-dif 3577  df-in 3581  df-nul 3916

This theorem is referenced by:  disjel  4023  disj4  4025  uneqdifeq  4057  uneqdifeqOLD  4058  difprsn1  4330  diftpsn3  4332  diftpsn3OLD  4333  ssunsn2  4359  orddif  5820  php  8144  hartogslem1  8447  infeq5i  8533  cantnfp1lem3  8577  cda1dif  8998  infcda1  9015  ssxr  10107  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1eulem  18471  lbsextlem4  19161  opsrtoslem2  19485  alexsublem  21848  volun  23313  lhop1lem  23776  ex-dif  27280  difeq  29355  imadifxp  29414  disjdsct  29480  carsgclctunlem1  30379  probun  30481  ballotlemfp1  30553  bj-disj2r  33013  topdifinfeq  33198  finixpnum  33394  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem27  33436  asindmre  33495  kelac2  37635  pwfi2f1o  37666  iccdifioo  39741  iccdifprioo  39742