Metamath Proof Explorer


Theorem eliunxp

Description: Membership in a union of Cartesian products. Analogue of elxp for nonconstant B ( x ) . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Assertion eliunxp ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 relxp Rel ( { 𝑥 } × 𝐵 )
2 1 rgenw 𝑥𝐴 Rel ( { 𝑥 } × 𝐵 )
3 reliun ( Rel 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∀ 𝑥𝐴 Rel ( { 𝑥 } × 𝐵 ) )
4 2 3 mpbir Rel 𝑥𝐴 ( { 𝑥 } × 𝐵 )
5 elrel ( ( Rel 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) → ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
6 4 5 mpan ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) → ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
7 6 pm4.71ri ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) )
8 nfiu1 𝑥 𝑥𝐴 ( { 𝑥 } × 𝐵 )
9 8 nfel2 𝑥 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 )
10 9 19.41 ( ∃ 𝑥 ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( ∃ 𝑥𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) )
11 19.41v ( ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) )
12 eleq1 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) )
13 opeliunxp ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥𝐴𝑦𝐵 ) )
14 12 13 bitrdi ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥𝐴𝑦𝐵 ) ) )
15 14 pm5.32i ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )
16 15 exbii ( ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )
17 11 16 bitr3i ( ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )
18 17 exbii ( ∃ 𝑥 ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑥𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )
19 7 10 18 3bitr2i ( 𝐶 𝑥𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥𝐴𝑦𝐵 ) ) )