Metamath Proof Explorer


Theorem eliunxp2

Description: Membership in a union of Cartesian products over its second component, analogous to eliunxp . (Contributed by AV, 30-Mar-2019)

Ref Expression
Assertion eliunxp2 C y B A × y x y C = x y x A y B

Proof

Step Hyp Ref Expression
1 relxp Rel A × y
2 1 rgenw y B Rel A × y
3 reliun Rel y B A × y y B Rel A × y
4 2 3 mpbir Rel y B A × y
5 elrel Rel y B A × y C y B A × y x y C = x y
6 4 5 mpan C y B A × y x y C = x y
7 excom y x C = x y x y C = x y
8 6 7 sylibr C y B A × y y x C = x y
9 8 pm4.71ri C y B A × y y x C = x y C y B A × y
10 nfiu1 _ y y B A × y
11 10 nfel2 y C y B A × y
12 11 19.41 y x C = x y C y B A × y y x C = x y C y B A × y
13 19.41v x C = x y C y B A × y x C = x y C y B A × y
14 eleq1 C = x y C y B A × y x y y B A × y
15 opeliun2xp x y y B A × y y B x A
16 15 biancomi x y y B A × y x A y B
17 14 16 bitrdi C = x y C y B A × y x A y B
18 17 pm5.32i C = x y C y B A × y C = x y x A y B
19 18 exbii x C = x y C y B A × y x C = x y x A y B
20 13 19 bitr3i x C = x y C y B A × y x C = x y x A y B
21 20 exbii y x C = x y C y B A × y y x C = x y x A y B
22 9 12 21 3bitr2i C y B A × y y x C = x y x A y B
23 excom y x C = x y x A y B x y C = x y x A y B
24 22 23 bitri C y B A × y x y C = x y x A y B