Theorem dfun2 2240

Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 2241 and dfss4 2239 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation \ (class difference).

Assertion

Ref	Expression
dfun2	|- (A u. B) = (V \ ((V \ A) \ B))

Proof of Theorem dfun2

Step	Hyp	Ref	Expression
1		eldif 2054	. . . . . . 7 |- (x e. (V \ A) <-> (x e. V /\ -. x e. A))
2		visset 1810	. . . . . . 7 |- x e. V
3	1, 2	mpbiran 727	. . . . . 6 |- (x e. (V \ A) <-> -. x e. A)
4	3	anbi1i 481	. . . . 5 |- ((x e. (V \ A) /\ -. x e. B) <-> (-. x e. A /\ -. x e. B))
5		eldif 2054	. . . . 5 |- (x e. ((V \ A) \ B) <-> (x e. (V \ A) /\ -. x e. B))
6		ioran 306	. . . . 5 |- (-. (x e. A \/ x e. B) <-> (-. x e. A /\ -. x e. B))
7	4, 5, 6	3bitr4 183	. . . 4 |- (x e. ((V \ A) \ B) <-> -. (x e. A \/ x e. B))
8	7	con2bii 221	. . 3 |- ((x e. A \/ x e. B) <-> -. x e. ((V \ A) \ B))
9		elun 2170	. . 3 |- (x e. (A u. B) <-> (x e. A \/ x e. B))
10		eldif 2054	. . . 4 |- (x e. (V \ ((V \ A) \ B)) <-> (x e. V /\ -. x e. ((V \ A) \ B)))
11	10, 2	mpbiran 727	. . 3 |- (x e. (V \ ((V \ A) \ B)) <-> -. x e. ((V \ A) \ B))
12	8, 9, 11	3bitr4 183	. 2 |- (x e. (A u. B) <-> x e. (V \ ((V \ A) \ B)))
13	12	eqriv 1473	1 |- (A u. B) = (V \ ((V \ A) \ B))

Syntax hints:  -. wn 2   \/ wo 222   /\ wa 223   = wceq 955   e. wcel 957  Vcvv 1808   \ cdif 2041   u. cun 2042

This theorem is referenced by:  dfun3 2243  dfin3 2244

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-or 224  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-un 2047

Copyright terms: Public domain