Theorem disj 3803

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 3419	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i 2456	. . 3 |- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1 2573	. . 3 |- ( { x | ( x e. A /\ x e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
4		imnan 422	. . . . 5 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
5		noel 3725	. . . . . 6 |- -. x e. (/)
6	5	nbn 347	. . . . 5 |- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7	4, 6	bitr2i 250	. . . 4 |- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
8	7	albii 1611	. . 3 |- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
9	2, 3, 8	3bitri 271	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10		df-ral 2797	. 2 |- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
11	9, 10	bitr4i 252	1 |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1368   = wceq 1370   e. wcel 1757   {cab 2435   A.wral 2792   i^i cin 3411   (/)c0 3721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ral 2797  df-v 3056  df-dif 3415  df-in 3419  df-nul 3722

This theorem is referenced by:  disjr  3804  disj1  3805  disjne  3808  onxpdisj  5004  onint  6492  zfreg  7897  kmlem4  8409  fin23lem30  8598  fin23lem31  8599  isf32lem3  8611  fpwwe2  8897  renfdisj  9524  injresinjlem  11725  metdsge  20527  spthispth  23593  subfacp1lem1  27187  dfpo2  27685  stoweidlem26  29945  stoweidlem59  29978  otiunsndisj  30256  otiunsndisjX  30257  f0rn0  30265  2spotdisj  30778  2spotiundisj  30779  2spotmdisj  30785