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	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) )