Theorem xpdifid 6120

Description: The set of distinct couples in a Cartesian product. (Contributed by Thierry Arnoux, 25-May-2019.)

Assertion

Ref	Expression
xpdifid	⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem xpdifid

Dummy variables 𝑖 𝑗 𝑝 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5656	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
2	1	rexbii 3097	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
3		rexcom4 3271	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
4		rexcom4 3271	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
5	4	exbii 1850	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
6	2, 3, 5	3bitri 296	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
7		eliun 4958	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})))
8		eldif 3920	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ))
9		opelxp 5669	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		df-br 5106	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ I )
11		vex 3449	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	11	ideq 5808	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ 𝑖 = 𝑗)
13	10, 12	bitr3i 276	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 = 𝑗)
14	13	necon3bbii 2991	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 ≠ 𝑗)
15	9, 14	anbi12i 627	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
16	8, 15	bitri 274	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
17	16	anbi2i 623	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
18	17	2exbii 1851	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
19		eldifi 4086	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → 𝑝 ∈ (𝐴 × 𝐵))
20		elxpi 5655	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
21		simpl 483	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
22	21	2eximi 1838	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
23	19, 20, 22	3syl 18	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	ancli 549	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
25		19.42vv 1961	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
26	24, 25	sylibr 233	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
27		ancom 461	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )))
28		eleq1 2825	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
29	28	adantl 482	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
30	29	pm5.32da 579	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
31	27, 30	bitrid 282	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
32	31	2exbidv 1927	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
33	26, 32	mpbid 231	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
34	28	biimpar 478	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
35	34	exlimivv 1935	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
36	33, 35	impbii 208	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
37		r19.42v 3187	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
38		simprl 769	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ {𝑦})
39		velsn 4602	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑦} ↔ 𝑖 = 𝑦)
40	38, 39	sylib 217	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 = 𝑦)
41		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ∈ 𝐴)
42	40, 41	eqeltrd 2838	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ 𝐴)
43		simprr 771	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ (𝐵 ∖ {𝑦}))
44	43	eldifad 3922	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ 𝐵)
45	43	eldifbd 3923	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ¬ 𝑗 ∈ {𝑦})
46		velsn 4602	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
47	46	necon3bbii 2991	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑗 ∈ {𝑦} ↔ 𝑗 ≠ 𝑦)
48	45, 47	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ≠ 𝑦)
49	48	necomd 2999	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ≠ 𝑗)
50	40, 49	eqnetrd 3011	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ≠ 𝑗)
51	42, 44, 50	jca31 515	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
52	51	adantll 712	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
53		sneq 4596	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
54	53	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
55	53	difeq2d 4082	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦}))
56	55	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑦})))
57	54, 56	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))))
58	57	cbvrexvw 3226	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
59	58	biimpi 215	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
60	52, 59	r19.29a 3159	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
61		simpll 765	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴)
62		vsnid 4623	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
63	62	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ {𝑖})
64		simplr 767	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐵)
65		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗)
66	65	necomd 2999	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ≠ 𝑖)
67		velsn 4602	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑖} ↔ 𝑗 = 𝑖)
68	67	necon3bbii 2991	. . . . . . . . . . 11 ⊢ (¬ 𝑗 ∈ {𝑖} ↔ 𝑗 ≠ 𝑖)
69	66, 68	sylibr 233	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ¬ 𝑗 ∈ {𝑖})
70	64, 69	eldifd 3921	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ (𝐵 ∖ {𝑖}))
71		sneq 4596	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
72	71	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
73	71	difeq2d 4082	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑖}))
74	73	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑖})))
75	72, 74	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))))
76	75	rspcev 3581	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
77	61, 63, 70, 76	syl12anc 835	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
78	60, 77	impbii 208	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
79	78	anbi2i 623	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
80	37, 79	bitri 274	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
81	80	2exbii 1851	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
82	18, 36, 81	3bitr4i 302	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
83	6, 7, 82	3bitr4i 302	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
84	83	eqriv 2733	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )

Syntax hints:  ¬ wn 3   ↔ wb 205   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3073   ∖ cdif 3907  {csn 4586  ⟨cop 4592  ∪ ciun 4954   class class class wbr 5105   I cid 5530   × cxp 5631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-iun 4956  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640

This theorem is referenced by:  tglnfn  27489