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) Avoid using unipr to prove it from uniprg . (Revised by BJ, 1-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑦 ∈ V
2	1	elpr	⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
3	2	anbi2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) )
4		ancom	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) ↔ ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) )
5		andir	⊢ ( ( ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ∧ 𝑥 ∈ 𝑦 ) ↔ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
6	4 5	bitri	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) ↔ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
7	3 6	bitri	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
8	7	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ∃ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
9		19.43	⊢ ( ∃ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
10	8 9	bitri	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
11		clel3g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ) )
12	11	bicomd	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝐴 ) )
13	12	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝐴 ) )
14		clel3g	⊢ ( 𝐵 ∈ 𝑊 → ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) )
15	14	bicomd	⊢ ( 𝐵 ∈ 𝑊 → ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝐵 ) )
16	15	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ↔ 𝑥 ∈ 𝐵 ) )
17	13 16	orbi12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ∨ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) )
18	10 17	bitrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ) )
19	18	abbidv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) } )
20		df-uni	⊢ ∪ { 𝐴 , 𝐵 } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) }
21		df-un	⊢ ( 𝐴 ∪ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) }
22	19 20 21	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )