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

Theorem reldisj 3870
 Description: Two ways of saying that two classes are disjoint, using the complement of relative to a universe . (Contributed by NM, 15-Feb-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
Assertion
Ref Expression
reldisj

Proof of Theorem reldisj
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfss2 3492 . . . 4
2 pm5.44 911 . . . . . 6
3 eldif 3485 . . . . . . 7
43imbi2i 312 . . . . . 6
52, 4syl6bbr 263 . . . . 5
65sps 1865 . . . 4
71, 6sylbi 195 . . 3
87albidv 1713 . 2
9 disj1 3869 . 2
10 dfss2 3492 . 2
118, 9, 103bitr4g 288 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  \cdif 3472  i^icin 3474  C_wss 3475   c0 3784 This theorem is referenced by:  disj2  3874  oacomf1olem  7232  domdifsn  7620  elfiun  7910  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  ssxr  9675  structcnvcnv  14643  fidomndrng  17956  elcls  19574  ist1-2  19848  nrmsep2  19857  nrmsep  19858  isnrm3  19860  isreg2  19878  hauscmplem  19906  connsub  19922  iunconlem  19928  llycmpkgen2  20051  hausdiag  20146  trfil3  20389  isufil2  20409  filufint  20421  blcld  21008  i1fima2  22086  i1fd  22088  usgrares1  24410  nbgrassvwo  24437  nbgrassvwo2  24438  itg2addnclem2  30067 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-ss 3489  df-nul 3785
 Copyright terms: Public domain W3C validator