# Metamath Proof Explorer

## 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 { 𝐴 , 𝐵 } = ( 𝐴𝐵 )