Metamath Proof Explorer

Theorem opeliunxp2f

Description: Membership in a union of Cartesian products, using bound-variable hypothesis for E instead of distinct variable conditions as in opeliunxp2 . (Contributed by AV, 25-Oct-2020)

Ref Expression
Hypotheses opeliunxp2f.f ⊢ Ⅎ _ x E
opeliunxp2f.e ⊢ x = C → B = E
Assertion opeliunxp2f ⊢ C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E

Proof

Step Hyp Ref Expression
1 opeliunxp2f.f ⊢ Ⅎ _ x E
2 opeliunxp2f.e ⊢ x = C → B = E
3 df-br ⊢ C ⋃ x ∈ A x × B D ↔ C D ∈ ⋃ x ∈ A x × B
4 relxp ⊢ Rel ⁡ x × B
5 4 rgenw ⊢ ∀ x ∈ A Rel ⁡ x × B
6 reliun ⊢ Rel ⁡ ⋃ x ∈ A x × B ↔ ∀ x ∈ A Rel ⁡ x × B
7 5 6 mpbir ⊢ Rel ⁡ ⋃ x ∈ A x × B
8 7 brrelex1i ⊢ C ⋃ x ∈ A x × B D → C ∈ V
9 3 8 sylbir ⊢ C D ∈ ⋃ x ∈ A x × B → C ∈ V
10 elex ⊢ C ∈ A → C ∈ V
11 10 adantr ⊢ C ∈ A ∧ D ∈ E → C ∈ V
12 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A x × B
13 12 nfel2 ⊢ Ⅎ x C D ∈ ⋃ x ∈ A x × B
14 nfv ⊢ Ⅎ x C ∈ A
15 1 nfel2 ⊢ Ⅎ x D ∈ E
16 14 15 nfan ⊢ Ⅎ x C ∈ A ∧ D ∈ E
17 13 16 nfbi ⊢ Ⅎ x C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
18 opeq1 ⊢ x = C → x D = C D
19 18 eleq1d ⊢ x = C → x D ∈ ⋃ x ∈ A x × B ↔ C D ∈ ⋃ x ∈ A x × B
20 eleq1 ⊢ x = C → x ∈ A ↔ C ∈ A
21 2 eleq2d ⊢ x = C → D ∈ B ↔ D ∈ E
22 20 21 anbi12d ⊢ x = C → x ∈ A ∧ D ∈ B ↔ C ∈ A ∧ D ∈ E
23 19 22 bibi12d ⊢ x = C → x D ∈ ⋃ x ∈ A x × B ↔ x ∈ A ∧ D ∈ B ↔ C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
24 opeliunxp ⊢ x D ∈ ⋃ x ∈ A x × B ↔ x ∈ A ∧ D ∈ B
25 17 23 24 vtoclg1f ⊢ C ∈ V → C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E
26 9 11 25 pm5.21nii ⊢ C D ∈ ⋃ x ∈ A x × B ↔ C ∈ A ∧ D ∈ E