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 AVBWAB=AB

Proof

Step Hyp Ref Expression
1 vex yV
2 1 elpr yABy=Ay=B
3 2 anbi2i xyyABxyy=Ay=B
4 ancom xyy=Ay=By=Ay=Bxy
5 andir y=Ay=Bxyy=Axyy=Bxy
6 4 5 bitri xyy=Ay=By=Axyy=Bxy
7 3 6 bitri xyyABy=Axyy=Bxy
8 7 exbii yxyyAByy=Axyy=Bxy
9 19.43 yy=Axyy=Bxyyy=Axyyy=Bxy
10 8 9 bitri yxyyAByy=Axyyy=Bxy
11 clel3g AVxAyy=Axy
12 11 bicomd AVyy=AxyxA
13 12 adantr AVBWyy=AxyxA
14 clel3g BWxByy=Bxy
15 14 bicomd BWyy=BxyxB
16 15 adantl AVBWyy=BxyxB
17 13 16 orbi12d AVBWyy=Axyyy=BxyxAxB
18 10 17 bitrid AVBWyxyyABxAxB
19 18 abbidv AVBWx|yxyyAB=x|xAxB
20 df-uni AB=x|yxyyAB
21 df-un AB=x|xAxB
22 19 20 21 3eqtr4g AVBWAB=AB