Theorem unipr

Description: The union of a pair is the union of its members. Proposition 5.7 of TakeutiZaring p. 16. (Contributed by NM, 23-Aug-1993)

	Ref	Expression
Hypotheses	unipr.1	|- A e. _V
	unipr.2	|- B e. _V
Assertion	unipr	|- U. { A , B } = ( A u. B )

Proof

Step	Hyp	Ref	Expression
1		unipr.1	|- A e. _V
2		unipr.2	|- B e. _V
3		19.43	|- ( E. y ( ( x e. y /\ y = A ) \/ ( x e. y /\ y = B ) ) <-> ( E. y ( x e. y /\ y = A ) \/ E. y ( x e. y /\ y = B ) ) )
4		vex	|- y e. _V
5	4	elpr	|- ( y e. { A , B } <-> ( y = A \/ y = B ) )
6	5	anbi2i	|- ( ( x e. y /\ y e. { A , B } ) <-> ( x e. y /\ ( y = A \/ y = B ) ) )
7		andi	|- ( ( x e. y /\ ( y = A \/ y = B ) ) <-> ( ( x e. y /\ y = A ) \/ ( x e. y /\ y = B ) ) )
8	6 7	bitri	|- ( ( x e. y /\ y e. { A , B } ) <-> ( ( x e. y /\ y = A ) \/ ( x e. y /\ y = B ) ) )
9	8	exbii	|- ( E. y ( x e. y /\ y e. { A , B } ) <-> E. y ( ( x e. y /\ y = A ) \/ ( x e. y /\ y = B ) ) )
10	1	clel3	|- ( x e. A <-> E. y ( y = A /\ x e. y ) )
11		exancom	|- ( E. y ( y = A /\ x e. y ) <-> E. y ( x e. y /\ y = A ) )
12	10 11	bitri	|- ( x e. A <-> E. y ( x e. y /\ y = A ) )
13	2	clel3	|- ( x e. B <-> E. y ( y = B /\ x e. y ) )
14		exancom	|- ( E. y ( y = B /\ x e. y ) <-> E. y ( x e. y /\ y = B ) )
15	13 14	bitri	|- ( x e. B <-> E. y ( x e. y /\ y = B ) )
16	12 15	orbi12i	|- ( ( x e. A \/ x e. B ) <-> ( E. y ( x e. y /\ y = A ) \/ E. y ( x e. y /\ y = B ) ) )
17	3 9 16	3bitr4ri	|- ( ( x e. A \/ x e. B ) <-> E. y ( x e. y /\ y e. { A , B } ) )
18	17	abbii	|- { x | ( x e. A \/ x e. B ) } = { x | E. y ( x e. y /\ y e. { A , B } ) }
19		df-un	|- ( A u. B ) = { x | ( x e. A \/ x e. B ) }
20		df-uni	|- U. { A , B } = { x | E. y ( x e. y /\ y e. { A , B } ) }
21	18 19 20	3eqtr4ri	|- U. { A , B } = ( A u. B )