This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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