Theorem disj 3816

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 3422	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i 2466	. . 3 |- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1 2571	. . 3 |- ( { x | ( x e. A /\ x e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
4		imnan 428	. . . . 5 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
5		noel 3746	. . . . . 6 |- -. x e. (/)
6	5	nbn 353	. . . . 5 |- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7	4, 6	bitr2i 258	. . . 4 |- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
8	7	albii 1701	. . 3 |- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
9	2, 3, 8	3bitri 279	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10		df-ral 2753	. 2 |- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
11	9, 10	bitr4i 260	1 |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1452   = wceq 1454   e. wcel 1897   {cab 2447   A.wral 2748   i^i cin 3414   (/)c0 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ral 2753  df-v 3058  df-dif 3418  df-in 3422  df-nul 3743

This theorem is referenced by:  disjr  3817  disj1  3818  disjne  3821  otiunsndisj  4720  onxpdisj  5560  f0rn0  5790  onint  6648  zfreg  8135  kmlem4  8608  fin23lem30  8797  fin23lem31  8798  isf32lem3  8810  fpwwe2  9093  renfdisj  9719  fvinim0ffz  12054  metdsge  21914  metdsgeOLD  21929  spthispth  25351  2spotdisj  25837  2spotiundisj  25838  2spotmdisj  25844  subfacp1lem1  29950  dfpo2  30443  dvmptfprodlem  37856  stoweidlem26  37923  stoweidlem59  37957  iundjiunlem  38334  otiunsndisjX  39045