MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disj Unicode version

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
StepHypRef Expression
1 df-in 3482 . . . 4
21eqeq1i 2464 . . 3
3 abeq1 2582 . . 3
4 imnan 422 . . . . 5
5 noel 3788 . . . . . 6
65nbn 347 . . . . 5
74, 6bitr2i 250 . . . 4
87albii 1640 . . 3
92, 3, 83bitri 271 . 2
10 df-ral 2812 . 2
119, 10bitr4i 252 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator