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

Proof

Step Hyp Ref Expression
1 opeliunxp2.1 ⊢ x = C → B = E
2 df-br ⊢ C ⋃ x ∈ A x × B D ↔ C D ∈ ⋃ x ∈ A x × B
3 relxp ⊢ Rel ⁡ x × B
4 3 rgenw ⊢ ∀ x ∈ A Rel ⁡ x × B
5 reliun ⊢ Rel ⁡ ⋃ x ∈ A x × B ↔ ∀ x ∈ A Rel ⁡ x × B
6 4 5 mpbir ⊢ Rel ⁡ ⋃ x ∈ A x × B
7 6 brrelex1i ⊢ C ⋃ x ∈ A x × B D → C ∈ V
8 2 7 sylbir ⊢ C D ∈ ⋃ x ∈ A x × B → C ∈ V
9 elex ⊢ C ∈ A → C ∈ V
10 9 adantr ⊢ C ∈ A ∧ D ∈ E → C ∈ V
11 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A x × B
12 11 nfel2 ⊢ Ⅎ x C D ∈ ⋃ x ∈ A x × B
13 nfv ⊢ Ⅎ x C ∈ A ∧ D ∈ E
14 12 13 nfbi ⊢ Ⅎ x C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
15 opeq1 ⊢ x = C → x D = C D
16 15 eleq1d ⊢ x = C → x D ∈ ⋃ x ∈ A x × B ↔ C D ∈ ⋃ x ∈ A x × 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 → x D ∈ ⋃ x ∈ A x × B ↔ x ∈ A ∧ D ∈ B ↔ C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
21 opeliunxp ⊢ x D ∈ ⋃ x ∈ A x × B ↔ x ∈ A ∧ D ∈ B
22 14 20 21 vtoclg1f ⊢ C ∈ V → C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
23 8 10 22 pm5.21nii ⊢ C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E