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	⊢ 𝐴 ∈ V
	unipr.2	⊢ 𝐵 ∈ V
Assertion	unipr	⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		unipr.1	⊢ 𝐴 ∈ V
2		unipr.2	⊢ 𝐵 ∈ V
3		19.43	⊢ ( ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) )
4		vex	⊢ 𝑦 ∈ V
5	4	elpr	⊢ ( 𝑦 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) )
6	5	anbi2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) )
7		andi	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( 𝑦 = 𝐴 ∨ 𝑦 = 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) )
8	6 7	bitri	⊢ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) )
9	8	exbii	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) ↔ ∃ 𝑦 ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) )
10	1	clel3	⊢ ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
11		exancom	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) )
12	10 11	bitri	⊢ ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) )
13	2	clel3	⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) )
14		exancom	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) )
15	13 14	bitri	⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) )
16	12 15	orbi12i	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ↔ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) ∨ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 = 𝐵 ) ) )
17	3 9 16	3bitr4ri	⊢ ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) )
18	17	abbii	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) }
19		df-un	⊢ ( 𝐴 ∪ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) }
20		df-uni	⊢ ∪ { 𝐴 , 𝐵 } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ { 𝐴 , 𝐵 } ) }
21	18 19 20	3eqtr4ri	⊢ ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 )