Theorem opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Assertion	opeliunxp	⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) }
2	1	eleq2i	⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝐶 ⟩ ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) } )
3		opex	⊢ ⟨ 𝑥 , 𝐶 ⟩ ∈ V
4		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) )
5		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) )
6		nfs1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴
7		nfcv	⊢ Ⅎ 𝑥 { 𝑧 }
8		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
9	7 8	nfxp	⊢ Ⅎ 𝑥 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
10	9	nfcri	⊢ Ⅎ 𝑥 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
11	6 10	nfan	⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
12		sbequ12	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ) )
13		sneq	⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
14		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
15	13 14	xpeq12d	⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × 𝐵 ) = ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
16	15	eleq2d	⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
17	12 16	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
18	5 11 17	cbvexv1	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
19	4 18	bitri	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
20		eleq1	⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
21	20	anbi2d	⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
22	21	exbidv	⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
23	19 22	syl5bb	⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
24	3 23	elab	⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) } ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
25		opelxp	⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
26	25	anbi2i	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
27		an12	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
28		velsn	⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
29		equcom	⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
30	28 29	bitri	⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑧 = 𝑥 )
31	30	anbi1i	⊢ ( ( 𝑥 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
32	26 27 31	3bitri	⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
33	32	exbii	⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
34		sbequ12r	⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
35	14	equcoms	⊢ ( 𝑧 = 𝑥 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
36	35	eqcomd	⊢ ( 𝑧 = 𝑥 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = 𝐵 )
37	36	eleq2d	⊢ ( 𝑧 = 𝑥 → ( 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ 𝐶 ∈ 𝐵 ) )
38	34 37	anbi12d	⊢ ( 𝑧 = 𝑥 → ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )
39	38	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )
40	33 39	bitri	⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )
41	2 24 40	3bitri	⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )