# 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 ( 𝑥 = 𝐶𝐵 = 𝐸 )
Assertion opeliunxp2 ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) )

### Proof

Step Hyp Ref Expression
1 opeliunxp2.1 ( 𝑥 = 𝐶𝐵 = 𝐸 )
2 df-br ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) )
3 relxp Rel ( { 𝑥 } × 𝐵 )
4 3 rgenw 𝑥𝐴 Rel ( { 𝑥 } × 𝐵 )
5 reliun ( Rel 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∀ 𝑥𝐴 Rel ( { 𝑥 } × 𝐵 ) )
6 4 5 mpbir Rel 𝑥𝐴 ( { 𝑥 } × 𝐵 )
7 6 brrelex1i ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) 𝐷𝐶 ∈ V )
8 2 7 sylbir ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) → 𝐶 ∈ V )
9 elex ( 𝐶𝐴𝐶 ∈ V )
10 9 adantr ( ( 𝐶𝐴𝐷𝐸 ) → 𝐶 ∈ V )
11 nfiu1 𝑥 𝑥𝐴 ( { 𝑥 } × 𝐵 )
12 11 nfel2 𝑥𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 )
13 nfv 𝑥 ( 𝐶𝐴𝐷𝐸 )
14 12 13 nfbi 𝑥 ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) )
15 opeq1 ( 𝑥 = 𝐶 → ⟨ 𝑥 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
16 15 eleq1d ( 𝑥 = 𝐶 → ( ⟨ 𝑥 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) )
17 eleq1 ( 𝑥 = 𝐶 → ( 𝑥𝐴𝐶𝐴 ) )
18 1 eleq2d ( 𝑥 = 𝐶 → ( 𝐷𝐵𝐷𝐸 ) )
19 17 18 anbi12d ( 𝑥 = 𝐶 → ( ( 𝑥𝐴𝐷𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) ) )
20 16 19 bibi12d ( 𝑥 = 𝐶 → ( ( ⟨ 𝑥 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥𝐴𝐷𝐵 ) ) ↔ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) ) ) )
21 opeliunxp ( ⟨ 𝑥 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥𝐴𝐷𝐵 ) )
22 14 20 21 vtoclg1f ( 𝐶 ∈ V → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) ) )
23 8 10 22 pm5.21nii ( ⟨ 𝐶 , 𝐷 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶𝐴𝐷𝐸 ) )