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	syl6bb	⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
15	14	pm5.32i	⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
16	15	exbii	⊢ ( ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
17	11 16	bitr3i	⊢ ( ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
18	17	exbii	⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
19	7 10 18	3bitr2i	⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )