Metamath Proof Explorer

Theorem uniprOLD

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

Ref Expression
Hypotheses unipr.1 ⊢A∈V
unipr.2 ⊢B∈V
Assertion uniprOLD ⊢⋃AB=A∪B

Proof

Step Hyp Ref Expression
1 unipr.1 ⊢A∈V
2 unipr.2 ⊢B∈V
3 19.43 ⊢∃yx∈y∧y=A∨x∈y∧y=B↔∃yx∈y∧y=A∨∃yx∈y∧y=B
4 vex ⊢y∈V
5 4 elpr ⊢y∈AB↔y=A∨y=B
6 5 anbi2i ⊢x∈y∧y∈AB↔x∈y∧y=A∨y=B
7 andi ⊢x∈y∧y=A∨y=B↔x∈y∧y=A∨x∈y∧y=B
8 6 7 bitri ⊢x∈y∧y∈AB↔x∈y∧y=A∨x∈y∧y=B
9 8 exbii ⊢∃yx∈y∧y∈AB↔∃yx∈y∧y=A∨x∈y∧y=B
10 1 clel3 ⊢x∈A↔∃yy=A∧x∈y
11 exancom ⊢∃yy=A∧x∈y↔∃yx∈y∧y=A
12 10 11 bitri ⊢x∈A↔∃yx∈y∧y=A
13 2 clel3 ⊢x∈B↔∃yy=B∧x∈y
14 exancom ⊢∃yy=B∧x∈y↔∃yx∈y∧y=B
15 13 14 bitri ⊢x∈B↔∃yx∈y∧y=B
16 12 15 orbi12i ⊢x∈A∨x∈B↔∃yx∈y∧y=A∨∃yx∈y∧y=B
17 3 9 16 3bitr4ri ⊢x∈A∨x∈B↔∃yx∈y∧y∈AB
18 17 abbii ⊢x|x∈A∨x∈B=x|∃yx∈y∧y∈AB
19 df-un ⊢A∪B=x|x∈A∨x∈B
20 df-uni ⊢⋃AB=x|∃yx∈y∧y∈AB
21 18 19 20 3eqtr4ri ⊢⋃AB=A∪B