Theorem disj 4017

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 3581	. . . 4 |- ( A i^i B ) = { x | ( x e. A /\ x e. B ) }
2	1	eqeq1i 2627	. . 3 |- ( ( A i^i B ) = (/) <-> { x | ( x e. A /\ x e. B ) } = (/) )
3		abeq1 2733	. . 3 |- ( { x | ( x e. A /\ x e. B ) } = (/) <-> A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
4		imnan 438	. . . . 5 |- ( ( x e. A -> -. x e. B ) <-> -. ( x e. A /\ x e. B ) )
5		noel 3919	. . . . . 6 |- -. x e. (/)
6	5	nbn 362	. . . . 5 |- ( -. ( x e. A /\ x e. B ) <-> ( ( x e. A /\ x e. B ) <-> x e. (/) ) )
7	4, 6	bitr2i 265	. . . 4 |- ( ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> ( x e. A -> -. x e. B ) )
8	7	albii 1747	. . 3 |- ( A. x ( ( x e. A /\ x e. B ) <-> x e. (/) ) <-> A. x ( x e. A -> -. x e. B ) )
9	2, 3, 8	3bitri 286	. 2 |- ( ( A i^i B ) = (/) <-> A. x ( x e. A -> -. x e. B ) )
10		df-ral 2917	. 2 |- ( A. x e. A -. x e. B <-> A. x ( x e. A -> -. x e. B ) )
11	9, 10	bitr4i 267	1 |- ( ( A i^i B ) = (/) <-> A. x e. A -. x e. B )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   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:  disjr  4018  disj1  4019  disjne  4022  disjord  4641  disjiund  4643  otiunsndisj  4980  onxpdisj  5847  f0rn0  6090  onint  6995  zfreg  8500  zfregOLD  8502  kmlem4  8975  fin23lem30  9164  fin23lem31  9165  isf32lem3  9177  fpwwe2  9465  renfdisj  10098  fvinim0ffz  12587  s3iunsndisj  13707  metdsge  22652  2wspmdisj  27201  subfacp1lem1  31161  dfpo2  31645  dvmptfprodlem  40159  stoweidlem26  40243  stoweidlem59  40276  iundjiunlem  40676  otiunsndisjX  41298