Theorem uniprg

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

	Ref	Expression
Assertion	uniprg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
2	1	unieqd	⊢ ( 𝑥 = 𝐴 → ∪ { 𝑥 , 𝑦 } = ∪ { 𝐴 , 𝑦 } )
3		uneq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∪ 𝑦 ) = ( 𝐴 ∪ 𝑦 ) )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ∪ { 𝑥 , 𝑦 } = ( 𝑥 ∪ 𝑦 ) ↔ ∪ { 𝐴 , 𝑦 } = ( 𝐴 ∪ 𝑦 ) ) )
5		preq2	⊢ ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
6	5	unieqd	⊢ ( 𝑦 = 𝐵 → ∪ { 𝐴 , 𝑦 } = ∪ { 𝐴 , 𝐵 } )
7		uneq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 ∪ 𝑦 ) = ( 𝐴 ∪ 𝐵 ) )
8	6 7	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ∪ { 𝐴 , 𝑦 } = ( 𝐴 ∪ 𝑦 ) ↔ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) ) )
9		vex	⊢ 𝑥 ∈ V
10		vex	⊢ 𝑦 ∈ V
11	9 10	unipr	⊢ ∪ { 𝑥 , 𝑦 } = ( 𝑥 ∪ 𝑦 )
12	4 8 11	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )