# 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}\to {B}={E}$
Assertion opeliunxp2 ${⊢}⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)$

### Proof

Step Hyp Ref Expression
1 opeliunxp2.1 ${⊢}{x}={C}\to {B}={E}$
2 df-br ${⊢}{C}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right){D}↔⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$
3 relxp ${⊢}\mathrm{Rel}\left(\left\{{x}\right\}×{B}\right)$
4 3 rgenw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{x}\right\}×{B}\right)$
5 reliun ${⊢}\mathrm{Rel}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{Rel}\left(\left\{{x}\right\}×{B}\right)$
6 4 5 mpbir ${⊢}\mathrm{Rel}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$
7 6 brrelex1i ${⊢}{C}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right){D}\to {C}\in \mathrm{V}$
8 2 7 sylbir ${⊢}⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\to {C}\in \mathrm{V}$
9 elex ${⊢}{C}\in {A}\to {C}\in \mathrm{V}$
10 9 adantr ${⊢}\left({C}\in {A}\wedge {D}\in {E}\right)\to {C}\in \mathrm{V}$
11 nfiu1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$
12 11 nfel2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)$
13 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({C}\in {A}\wedge {D}\in {E}\right)$
14 12 13 nfbi ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)\right)$
15 opeq1 ${⊢}{x}={C}\to ⟨{x},{D}⟩=⟨{C},{D}⟩$
16 15 eleq1d ${⊢}{x}={C}\to \left(⟨{x},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)\right)$
17 eleq1 ${⊢}{x}={C}\to \left({x}\in {A}↔{C}\in {A}\right)$
18 1 eleq2d ${⊢}{x}={C}\to \left({D}\in {B}↔{D}\in {E}\right)$
19 17 18 anbi12d ${⊢}{x}={C}\to \left(\left({x}\in {A}\wedge {D}\in {B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)\right)$
20 16 19 bibi12d ${⊢}{x}={C}\to \left(\left(⟨{x},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({x}\in {A}\wedge {D}\in {B}\right)\right)↔\left(⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)\right)\right)$
21 opeliunxp ${⊢}⟨{x},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({x}\in {A}\wedge {D}\in {B}\right)$
22 14 20 21 vtoclg1f ${⊢}{C}\in \mathrm{V}\to \left(⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)\right)$
23 8 10 22 pm5.21nii ${⊢}⟨{C},{D}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({C}\in {A}\wedge {D}\in {E}\right)$