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

Distinct variable groups:   ,   ,

Proof of Theorem disj

Step	Hyp	Ref	Expression
1		df-in 3482	. . . 4
2	1	eqeq1i 2464	. . 3
3		abeq1 2582	. . 3
4		imnan 422	. . . . 5
5		noel 3788	. . . . . 6
6	5	nbn 347	. . . . 5
7	4, 6	bitr2i 250	. . . 4
8	7	albii 1640	. . 3
9	2, 3, 8	3bitri 271	. 2
10		df-ral 2812	. 2
11	9, 10	bitr4i 252	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442  A.wral 2807  i^icin 3474  c0 3784

This theorem is referenced by:  disjr  3868  disj1  3869  disjne  3872  otiunsndisj  4758  onxpdisj  5088  f0rn0  5775  onint  6630  zfreg  8042  kmlem4  8554  fin23lem30  8743  fin23lem31  8744  isf32lem3  8756  fpwwe2  9042  renfdisj  9668  injresinjlem  11925  metdsge  21353  spthispth  24575  2spotdisj  25061  2spotiundisj  25062  2spotmdisj  25068  subfacp1lem1  28623  dfpo2  29184  dvmptfprodlem  31741  stoweidlem26  31808  stoweidlem59  31841  otiunsndisjX  32301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-dif 3478  df-in 3482  df-nul 3785