Theorem dfun2

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

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

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		eldif	|- ( x e. ( _V \ A ) <-> ( x e. _V /\ -. x e. A ) )
3	1 2	mpbiran	|- ( x e. ( _V \ A ) <-> -. x e. A )
4	3	anbi1i	|- ( ( x e. ( _V \ A ) /\ -. x e. B ) <-> ( -. x e. A /\ -. x e. B ) )
5		eldif	|- ( x e. ( ( _V \ A ) \ B ) <-> ( x e. ( _V \ A ) /\ -. x e. B ) )
6		ioran	|- ( -. ( x e. A \/ x e. B ) <-> ( -. x e. A /\ -. x e. B ) )
7	4 5 6	3bitr4i	|- ( x e. ( ( _V \ A ) \ B ) <-> -. ( x e. A \/ x e. B ) )
8	7	con2bii	|- ( ( x e. A \/ x e. B ) <-> -. x e. ( ( _V \ A ) \ B ) )
9		eldif	|- ( x e. ( _V \ ( ( _V \ A ) \ B ) ) <-> ( x e. _V /\ -. x e. ( ( _V \ A ) \ B ) ) )
10	1 9	mpbiran	|- ( x e. ( _V \ ( ( _V \ A ) \ B ) ) <-> -. x e. ( ( _V \ A ) \ B ) )
11	8 10	bitr4i	|- ( ( x e. A \/ x e. B ) <-> x e. ( _V \ ( ( _V \ A ) \ B ) ) )
12	11	uneqri	|- ( A u. B ) = ( _V \ ( ( _V \ A ) \ B ) )