Theorem reldisj 3121

Description: Two ways of saying that two classes are disjoint, using the complement of B relative to a universe C. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
reldisj	|- (A C_ C -> ((A i^i B) = (/) <-> A C_ (C \ B)))

Proof of Theorem reldisj

Step	Hyp	Ref	Expression
1		dfss2 2841	. . . 4 |- (A C_ C <-> A.x(x e. A -> x e. C))
2		pm5.44 1012	. . . . . 6 |- ((x e. A -> x e. C) -> ((x e. A -> -. x e. B) <-> (x e. A -> (x e. C /\ -. x e. B))))
3		eldif 2840	. . . . . . 7 |- (x e. (C \ B) <-> (x e. C /\ -. x e. B))
4	3	imbi2i 297	. . . . . 6 |- ((x e. A -> x e. (C \ B)) <-> (x e. A -> (x e. C /\ -. x e. B)))
5	2, 4	syl6bbr 731	. . . . 5 |- ((x e. A -> x e. C) -> ((x e. A -> -. x e. B) <-> (x e. A -> x e. (C \ B))))
6	5	a4s 1619	. . . 4 |- (A.x(x e. A -> x e. C) -> ((x e. A -> -. x e. B) <-> (x e. A -> x e. (C \ B))))
7	1, 6	sylbi 225	. . 3 |- (A C_ C -> ((x e. A -> -. x e. B) <-> (x e. A -> x e. (C \ B))))
8	7	albidv 1925	. 2 |- (A C_ C -> (A.x(x e. A -> -. x e. B) <-> A.x(x e. A -> x e. (C \ B))))
9		disj1 3120	. 2 |- ((A i^i B) = (/) <-> A.x(x e. A -> -. x e. B))
10		dfss2 2841	. 2 |- (A C_ (C \ B) <-> A.x(x e. A -> x e. (C \ B)))
11	8, 9, 10	3bitr4g 745	1 |- (A C_ C -> ((A i^i B) = (/) <-> A C_ (C \ B)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588   \ cdif 2824   i^i cin 2826   C_ wss 2827  (/)c0 3082

This theorem is referenced by:  disj2 3124  ssxr 6899  elcls 9844  islp2 9889  clindistop 15740  connsub 16267  reconnlem1 16270  locfincomp 16338  ist1-2 16366  isnrm2 16376  isufil2 16389  ufileulem 16396  ufileu 16397  filufint 16398  fcluscf 16436  flimfnfcls 16439

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-ral 2359  df-v 2540  df-dif 2830  df-in 2834  df-ss 2836  df-nul 3083

Copyright terms: Public domain