Theorem disj 3867

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 3483	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i 2474	. . 3 |- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1 2592	. . 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 3789	. . . . . 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 1620	. . 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 2819	. 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 1377   = wceq 1379   e. wcel 1767   {cab 2452   A.wral 2814   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:  disjr  3868  disj1  3869  disjne  3872  otiunsndisj  4753  onxpdisj  5081  f0rn0  5768  onint  6608  zfreg  8017  kmlem4  8529  fin23lem30  8718  fin23lem31  8719  isf32lem3  8731  fpwwe2  9017  renfdisj  9643  injresinjlem  11889  metdsge  21088  spthispth  24251  2spotdisj  24738  2spotiundisj  24739  2spotmdisj  24745  subfacp1lem1  28263  dfpo2  28761  stoweidlem26  31326  stoweidlem59  31359  otiunsndisjX  31768