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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex | |
|
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 | |