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 
|- ( ( A e. V /\ B e. W ) -> U. { A , B } = ( A u. B ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 1 elpr 
 |-  ( y e. { A , B } <-> ( y = A \/ y = B ) )
3 2 anbi2i 
 |-  ( ( x e. y /\ y e. { A , B } ) <-> ( x e. y /\ ( y = A \/ y = B ) ) )
4 ancom 
 |-  ( ( x e. y /\ ( y = A \/ y = B ) ) <-> ( ( y = A \/ y = B ) /\ x e. y ) )
5 andir 
 |-  ( ( ( y = A \/ y = B ) /\ x e. y ) <-> ( ( y = A /\ x e. y ) \/ ( y = B /\ x e. y ) ) )
6 4 5 bitri 
 |-  ( ( x e. y /\ ( y = A \/ y = B ) ) <-> ( ( y = A /\ x e. y ) \/ ( y = B /\ x e. y ) ) )
7 3 6 bitri 
 |-  ( ( x e. y /\ y e. { A , B } ) <-> ( ( y = A /\ x e. y ) \/ ( y = B /\ x e. y ) ) )
8 7 exbii 
 |-  ( E. y ( x e. y /\ y e. { A , B } ) <-> E. y ( ( y = A /\ x e. y ) \/ ( y = B /\ x e. y ) ) )
9 19.43 
 |-  ( E. y ( ( y = A /\ x e. y ) \/ ( y = B /\ x e. y ) ) <-> ( E. y ( y = A /\ x e. y ) \/ E. y ( y = B /\ x e. y ) ) )
10 8 9 bitri 
 |-  ( E. y ( x e. y /\ y e. { A , B } ) <-> ( E. y ( y = A /\ x e. y ) \/ E. y ( y = B /\ x e. y ) ) )
11 clel3g 
 |-  ( A e. V -> ( x e. A <-> E. y ( y = A /\ x e. y ) ) )
12 11 bicomd 
 |-  ( A e. V -> ( E. y ( y = A /\ x e. y ) <-> x e. A ) )
13 12 adantr 
 |-  ( ( A e. V /\ B e. W ) -> ( E. y ( y = A /\ x e. y ) <-> x e. A ) )
14 clel3g 
 |-  ( B e. W -> ( x e. B <-> E. y ( y = B /\ x e. y ) ) )
15 14 bicomd 
 |-  ( B e. W -> ( E. y ( y = B /\ x e. y ) <-> x e. B ) )
16 15 adantl 
 |-  ( ( A e. V /\ B e. W ) -> ( E. y ( y = B /\ x e. y ) <-> x e. B ) )
17 13 16 orbi12d 
 |-  ( ( A e. V /\ B e. W ) -> ( ( E. y ( y = A /\ x e. y ) \/ E. y ( y = B /\ x e. y ) ) <-> ( x e. A \/ x e. B ) ) )
18 10 17 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( E. y ( x e. y /\ y e. { A , B } ) <-> ( x e. A \/ x e. B ) ) )
19 18 abbidv 
 |-  ( ( A e. V /\ B e. W ) -> { x | E. y ( x e. y /\ y e. { A , B } ) } = { x | ( x e. A \/ x e. B ) } )
20 df-uni 
 |-  U. { A , B } = { x | E. y ( x e. y /\ y e. { A , B } ) }
21 df-un 
 |-  ( A u. B ) = { x | ( x e. A \/ x e. B ) }
22 19 20 21 3eqtr4g 
 |-  ( ( A e. V /\ B e. W ) -> U. { A , B } = ( A u. B ) )