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.

Step	Hyp	Ref	Expression
1		dfss2 3492	. . . 4
2		pm5.44 911	. . . . . 6
3		eldif 3485	. . . . . . 7
4	3	imbi2i 312	. . . . . 6
5	2, 4	syl6bbr 263	. . . . 5
6	5	sps 1865	. . . 4
7	1, 6	sylbi 195	. . 3
8	7	albidv 1713	. 2
9		disj1 3869	. 2
10		dfss2 3492	. 2
11	8, 9, 10	3bitr4g 288	1

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