Theorem disj 3508

Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.)

Assertion

Ref	Expression
disj	|- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Distinct variable groups:   x, A   x, B

Proof of Theorem disj

Step	Hyp	Ref	Expression
1		df-in 3171	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i 2212	. . 3 |- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1 2314	. . 3 |- ( { x | ( x e. A /\ x e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
4		imnan 691	. . . . 5 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
5		noel 3463	. . . . . 6 |- -. x e. (/)
6	5	nbn 700	. . . . 5 |- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7	4, 6	bitr2i 185	. . . 4 |- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
8	7	albii 1492	. . 3 |- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
9	2, 3, 8	3bitri 206	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10		df-ral 2488	. 2 |- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
11	9, 10	bitr4i 187	1 |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1370   = wceq 1372   e. wcel 2175   {cab 2190   A.wral 2483   i^i cin 3164   (/)c0 3459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-v 2773  df-dif 3167  df-in 3171  df-nul 3460

This theorem is referenced by:  disjr  3509  disj1  3510  disjne  3513  f0rn0  5469  renfdisj  8131  fvinim0ffz  10368  xnn0nnen  10580  fxnn0nninf  10582  fprodsplitdc  11878  exmidunben  12768  dedekindeulemuub  15060  dedekindeulemlu  15064  dedekindicclemuub  15069  dedekindicclemlu  15073  ivthinclemdisj  15083  exmidsbthrlem  15923