Metamath Proof Explorer

Theorem opeliunxp2

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypothesis opeliunxp2.1 ⊢x=C→B=E
Assertion opeliunxp2 ⊢CD∈⋃x∈Ax×B↔C∈A∧D∈E

Proof

Step Hyp Ref Expression
1 opeliunxp2.1 ⊢x=C→B=E
2 df-br ⊢C⋃x∈Ax×BD↔CD∈⋃x∈Ax×B
3 relxp ⊢Rel⁡x×B
4 3 rgenw ⊢∀x∈ARel⁡x×B
5 reliun ⊢Rel⁡⋃x∈Ax×B↔∀x∈ARel⁡x×B
6 4 5 mpbir ⊢Rel⁡⋃x∈Ax×B
7 6 brrelex1i ⊢C⋃x∈Ax×BD→C∈V
8 2 7 sylbir ⊢CD∈⋃x∈Ax×B→C∈V
9 elex ⊢C∈A→C∈V
10 9 adantr ⊢C∈A∧D∈E→C∈V
11 nfiu1 ⊢Ⅎ_x⋃x∈Ax×B
12 11 nfel2 ⊢ℲxCD∈⋃x∈Ax×B
13 nfv ⊢ℲxC∈A∧D∈E
14 12 13 nfbi ⊢ℲxCD∈⋃x∈Ax×B↔C∈A∧D∈E
15 opeq1 ⊢x=C→xD=CD
16 15 eleq1d ⊢x=C→xD∈⋃x∈Ax×B↔CD∈⋃x∈Ax×B
17 eleq1 ⊢x=C→x∈A↔C∈A
18 1 eleq2d ⊢x=C→D∈B↔D∈E
19 17 18 anbi12d ⊢x=C→x∈A∧D∈B↔C∈A∧D∈E
20 16 19 bibi12d ⊢x=C→xD∈⋃x∈Ax×B↔x∈A∧D∈B↔CD∈⋃x∈Ax×B↔C∈A∧D∈E
21 opeliunxp ⊢xD∈⋃x∈Ax×B↔x∈A∧D∈B
22 14 20 21 vtoclg1f ⊢C∈V→CD∈⋃x∈Ax×B↔C∈A∧D∈E
23 8 10 22 pm5.21nii ⊢CD∈⋃x∈Ax×B↔C∈A∧D∈E