Metamath Proof Explorer

Theorem opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion opeliunxp ${⊢}⟨{x},{C}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({x}\in {A}\wedge {C}\in {B}\right)$

Proof

Step Hyp Ref Expression
1 df-iun ${⊢}\bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(\left\{{x}\right\}×{B}\right)\right\}$
2 1 eleq2i ${⊢}⟨{x},{C}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔⟨{x},{C}⟩\in \left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(\left\{{x}\right\}×{B}\right)\right\}$
3 opex ${⊢}⟨{x},{C}⟩\in \mathrm{V}$
4 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in \left(\left\{{x}\right\}×{B}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in \left(\left\{{x}\right\}×{B}\right)\right)$
5 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {y}\in \left(\left\{{x}\right\}×{B}\right)\right)$
6 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{x}\in {A}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}\right\}$
8 nfcsb1v
9 7 8 nfxp
10 9 nfcri
11 6 10 nfan
12 sbequ12 ${⊢}{x}={z}\to \left({x}\in {A}↔\left[{z}/{x}\right]{x}\in {A}\right)$
13 sneq ${⊢}{x}={z}\to \left\{{x}\right\}=\left\{{z}\right\}$
14 csbeq1a
15 13 14 xpeq12d
16 15 eleq2d
17 12 16 anbi12d
18 5 11 17 cbvexv1
19 4 18 bitri
20 eleq1
21 20 anbi2d
22 21 exbidv
23 19 22 syl5bb
24 3 23 elab
25 opelxp
26 25 anbi2i
27 an12
28 velsn ${⊢}{x}\in \left\{{z}\right\}↔{x}={z}$
29 equcom ${⊢}{x}={z}↔{z}={x}$
30 28 29 bitri ${⊢}{x}\in \left\{{z}\right\}↔{z}={x}$
31 30 anbi1i
32 26 27 31 3bitri
33 32 exbii
34 sbequ12r ${⊢}{z}={x}\to \left(\left[{z}/{x}\right]{x}\in {A}↔{x}\in {A}\right)$
35 14 equcoms
36 35 eqcomd
37 36 eleq2d
38 34 37 anbi12d
39 38 equsexvw
40 33 39 bitri
41 2 24 40 3bitri ${⊢}⟨{x},{C}⟩\in \bigcup _{{x}\in {A}}\left(\left\{{x}\right\}×{B}\right)↔\left({x}\in {A}\wedge {C}\in {B}\right)$