Metamath Proof Explorer

Theorem opeliun2xp

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

Ref Expression
Assertion opeliun2xp ⊢Cy∈⋃y∈BA×y↔y∈B∧C∈A

Proof

Step Hyp Ref Expression
1 df-iun ⊢⋃y∈BA×y=x|∃y∈Bx∈A×y
2 1 eleq2i ⊢Cy∈⋃y∈BA×y↔Cy∈x|∃y∈Bx∈A×y
3 opex ⊢Cy∈V
4 df-rex ⊢∃y∈Bx∈A×y↔∃yy∈B∧x∈A×y
5 nfv ⊢Ⅎzy∈B∧x∈A×y
6 nfs1v ⊢Ⅎyzyy∈B
7 nfcsb1v ⊢Ⅎ_y⦋z/y⦌A
8 nfcv ⊢Ⅎ_yz
9 7 8 nfxp ⊢Ⅎ_y⦋z/y⦌A×z
10 9 nfcri ⊢Ⅎyx∈⦋z/y⦌A×z
11 6 10 nfan ⊢Ⅎyzyy∈B∧x∈⦋z/y⦌A×z
12 sbequ12 ⊢y=z→y∈B↔zyy∈B
13 csbeq1a ⊢y=z→A=⦋z/y⦌A
14 sneq ⊢y=z→y=z
15 13 14 xpeq12d ⊢y=z→A×y=⦋z/y⦌A×z
16 15 eleq2d ⊢y=z→x∈A×y↔x∈⦋z/y⦌A×z
17 12 16 anbi12d ⊢y=z→y∈B∧x∈A×y↔zyy∈B∧x∈⦋z/y⦌A×z
18 5 11 17 cbvexv1 ⊢∃yy∈B∧x∈A×y↔∃zzyy∈B∧x∈⦋z/y⦌A×z
19 4 18 bitri ⊢∃y∈Bx∈A×y↔∃zzyy∈B∧x∈⦋z/y⦌A×z
20 eleq1 ⊢x=Cy→x∈⦋z/y⦌A×z↔Cy∈⦋z/y⦌A×z
21 20 anbi2d ⊢x=Cy→zyy∈B∧x∈⦋z/y⦌A×z↔zyy∈B∧Cy∈⦋z/y⦌A×z
22 21 exbidv ⊢x=Cy→∃zzyy∈B∧x∈⦋z/y⦌A×z↔∃zzyy∈B∧Cy∈⦋z/y⦌A×z
23 19 22 bitrid ⊢x=Cy→∃y∈Bx∈A×y↔∃zzyy∈B∧Cy∈⦋z/y⦌A×z
24 3 23 elab ⊢Cy∈x|∃y∈Bx∈A×y↔∃zzyy∈B∧Cy∈⦋z/y⦌A×z
25 opelxp ⊢Cy∈⦋z/y⦌A×z↔C∈⦋z/y⦌A∧y∈z
26 25 anbi2i ⊢zyy∈B∧Cy∈⦋z/y⦌A×z↔zyy∈B∧C∈⦋z/y⦌A∧y∈z
27 an13 ⊢zyy∈B∧C∈⦋z/y⦌A∧y∈z↔y∈z∧C∈⦋z/y⦌A∧zyy∈B
28 ancom ⊢C∈⦋z/y⦌A∧zyy∈B↔zyy∈B∧C∈⦋z/y⦌A
29 28 anbi2i ⊢y∈z∧C∈⦋z/y⦌A∧zyy∈B↔y∈z∧zyy∈B∧C∈⦋z/y⦌A
30 27 29 bitri ⊢zyy∈B∧C∈⦋z/y⦌A∧y∈z↔y∈z∧zyy∈B∧C∈⦋z/y⦌A
31 velsn ⊢y∈z↔y=z
32 equcom ⊢y=z↔z=y
33 31 32 bitri ⊢y∈z↔z=y
34 33 anbi1i ⊢y∈z∧zyy∈B∧C∈⦋z/y⦌A↔z=y∧zyy∈B∧C∈⦋z/y⦌A
35 26 30 34 3bitri ⊢zyy∈B∧Cy∈⦋z/y⦌A×z↔z=y∧zyy∈B∧C∈⦋z/y⦌A
36 35 exbii ⊢∃zzyy∈B∧Cy∈⦋z/y⦌A×z↔∃zz=y∧zyy∈B∧C∈⦋z/y⦌A
37 sbequ12r ⊢z=y→zyy∈B↔y∈B
38 13 equcoms ⊢z=y→A=⦋z/y⦌A
39 38 eqcomd ⊢z=y→⦋z/y⦌A=A
40 39 eleq2d ⊢z=y→C∈⦋z/y⦌A↔C∈A
41 37 40 anbi12d ⊢z=y→zyy∈B∧C∈⦋z/y⦌A↔y∈B∧C∈A
42 41 equsexvw ⊢∃zz=y∧zyy∈B∧C∈⦋z/y⦌A↔y∈B∧C∈A
43 36 42 bitri ⊢∃zzyy∈B∧Cy∈⦋z/y⦌A×z↔y∈B∧C∈A
44 2 24 43 3bitri ⊢Cy∈⋃y∈BA×y↔y∈B∧C∈A