Theorem disj 2914

Description: Two ways of saying that two classes are disjoint (have no members in common).

Assertion

Ref	Expression
disj	|- ((A i^i B) = (/) <-> A.x e. A -. x e. B)

Distinct variable groups:   x,A   x,B

Proof of Theorem disj

Step	Hyp	Ref	Expression
1		df-in 2603	. . . 4 |- (A i^i B) = {x | (x e. A /\ x e. B)}
2	1	eqeq1i 1891	. . 3 |- ((A i^i B) = (/) <-> {x | (x e. A /\ x e. B)} = (/))
3		abeq1 2000	. . 3 |- ({x | (x e. A /\ x e. B)} = (/) <-> A.x((x e. A /\ x e. B) <-> x e. (/)))
4		imnan 261	. . . . 5 |- ((x e. A -> -. x e. B) <-> -. (x e. A /\ x e. B))
5		noel 2879	. . . . . 6 |- -. x e. (/)
6	5	nbn 791	. . . . 5 |- (-. (x e. A /\ x e. B) <-> ((x e. A /\ x e. B) <-> x e. (/)))
7	4, 6	bitr2i 191	. . . 4 |- (((x e. A /\ x e. B) <-> x e. (/)) <-> (x e. A -> -. x e. B))
8	7	albii 1346	. . 3 |- (A.x((x e. A /\ x e. B) <-> x e. (/)) <-> A.x(x e. A -> -. x e. B))
9	2, 3, 8	3bitri 194	. 2 |- ((A i^i B) = (/) <-> A.x(x e. A -> -. x e. B))
10		df-ral 2109	. 2 |- (A.x e. A -. x e. B <-> A.x(x e. A -> -. x e. B))
11	9, 10	bitr4i 193	1 |- ((A i^i B) = (/) <-> A.x e. A -. x e. B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105   i^i cin 2592  (/)c0 2875

This theorem is referenced by:  disj1 2915  disjne 2919  disjneOLD 2920  dffr2 3627  dffr2OLD 3628  onint 3876  onxpdisj 4068  onxpdisjOLD 4069  zfreg 5698  zfreg2 5699  kmlem4 5930  renfdisj 6712  ssxrOLD 6715  qdensere 9027  bl2in 9120  lpbl 9157  imfstnrelc 14396  disjr 15675

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-v 2294  df-dif 2597  df-in 2603  df-nul 2876

Copyright terms: Public domain