Theorem uniprgOLD

Description: Obsolete version of unipr as of 1-Sep-2024. (Contributed by NM, 25-Aug-2006) (Proof modification is discouraged.) (New usage is discouraged.)

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

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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )