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 ⊢ C y ∈ ⋃ y ∈ B A × y ↔ y ∈ B ∧ C ∈ A

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ y ∈ B A × y = x | ∃ y ∈ B x ∈ A × y
2 1 eleq2i ⊢ C y ∈ ⋃ y ∈ B A × y ↔ C y ∈ x | ∃ y ∈ B x ∈ A × y
3 opex ⊢ C y ∈ V
4 df-rex ⊢ ∃ y ∈ B x ∈ A × y ↔ ∃ y y ∈ B ∧ x ∈ A × y
5 nfv ⊢ Ⅎ z y ∈ B ∧ x ∈ A × y
6 nfs1v ⊢ Ⅎ y z y y ∈ B
7 nfcsb1v ⊢ Ⅎ _ y ⦋ z / y⦌ A
8 nfcv ⊢ Ⅎ _ y z
9 7 8 nfxp ⊢ Ⅎ _ y ⦋ z / y⦌ A × z
10 9 nfcri ⊢ Ⅎ y x ∈ ⦋ z / y⦌ A × z
11 6 10 nfan ⊢ Ⅎ y z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z
12 sbequ12 ⊢ y = z → y ∈ B ↔ z y y ∈ 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 ↔ z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z
18 5 11 17 cbvexv1 ⊢ ∃ y y ∈ B ∧ x ∈ A × y ↔ ∃ z z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z
19 4 18 bitri ⊢ ∃ y ∈ B x ∈ A × y ↔ ∃ z z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z
20 eleq1 ⊢ x = C y → x ∈ ⦋ z / y⦌ A × z ↔ C y ∈ ⦋ z / y⦌ A × z
21 20 anbi2d ⊢ x = C y → z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z ↔ z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z
22 21 exbidv ⊢ x = C y → ∃ z z y y ∈ B ∧ x ∈ ⦋ z / y⦌ A × z ↔ ∃ z z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z
23 19 22 bitrid ⊢ x = C y → ∃ y ∈ B x ∈ A × y ↔ ∃ z z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z
24 3 23 elab ⊢ C y ∈ x | ∃ y ∈ B x ∈ A × y ↔ ∃ z z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z
25 opelxp ⊢ C y ∈ ⦋ z / y⦌ A × z ↔ C ∈ ⦋ z / y⦌ A ∧ y ∈ z
26 25 anbi2i ⊢ z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z ↔ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ∧ y ∈ z
27 an13 ⊢ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ∧ y ∈ z ↔ y ∈ z ∧ C ∈ ⦋ z / y⦌ A ∧ z y y ∈ B
28 ancom ⊢ C ∈ ⦋ z / y⦌ A ∧ z y y ∈ B ↔ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A
29 28 anbi2i ⊢ y ∈ z ∧ C ∈ ⦋ z / y⦌ A ∧ z y y ∈ B ↔ y ∈ z ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A
30 27 29 bitri ⊢ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ∧ y ∈ z ↔ y ∈ z ∧ z y y ∈ 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 ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ↔ z = y ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A
35 26 30 34 3bitri ⊢ z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z ↔ z = y ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A
36 35 exbii ⊢ ∃ z z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z ↔ ∃ z z = y ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A
37 sbequ12r ⊢ z = y → z y y ∈ 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 → z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ↔ y ∈ B ∧ C ∈ A
42 41 equsexvw ⊢ ∃ z z = y ∧ z y y ∈ B ∧ C ∈ ⦋ z / y⦌ A ↔ y ∈ B ∧ C ∈ A
43 36 42 bitri ⊢ ∃ z z y y ∈ B ∧ C y ∈ ⦋ z / y⦌ A × z ↔ y ∈ B ∧ C ∈ A
44 2 24 43 3bitri ⊢ C y ∈ ⋃ y ∈ B A × y ↔ y ∈ B ∧ C ∈ A