Theorem dfin2 2241

Description: An alternate definition of the intersection of two classes in terms of class difference, requiring no dummy variables. See comments under dfun2 2240. Another version is given by dfin4 2245.

Assertion

Ref	Expression
dfin2	|- (A i^i B) = (A \ (V \ B))

Proof of Theorem dfin2

Step	Hyp	Ref	Expression
1		eldif 2054	. . . . . 6 |- (x e. (V \ B) <-> (x e. V /\ -. x e. B))
2		visset 1810	. . . . . 6 |- x e. V
3	1, 2	mpbiran 727	. . . . 5 |- (x e. (V \ B) <-> -. x e. B)
4	3	con2bii 221	. . . 4 |- (x e. B <-> -. x e. (V \ B))
5	4	anbi2i 480	. . 3 |- ((x e. A /\ x e. B) <-> (x e. A /\ -. x e. (V \ B)))
6		elin 2204	. . 3 |- (x e. (A i^i B) <-> (x e. A /\ x e. B))
7		eldif 2054	. . 3 |- (x e. (A \ (V \ B)) <-> (x e. A /\ -. x e. (V \ B)))
8	5, 6, 7	3bitr4 183	. 2 |- (x e. (A i^i B) <-> x e. (A \ (V \ B)))
9	8	eqriv 1473	1 |- (A i^i B) = (A \ (V \ B))

Syntax hints:  -. wn 2   /\ wa 223   = wceq 955   e. wcel 957  Vcvv 1808   \ cdif 2041   i^i cin 2043

This theorem is referenced by:  dfun3 2243  dfin3 2244  invdif 2246  difundi 2254  difindi 2256

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-dif 2046  df-in 2048

Copyright terms: Public domain