Theorem xpdifid 6141

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 5661	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
2	1	rexbii 3076	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
3		rexcom4 3264	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
4		rexcom4 3264	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
5	4	exbii 1848	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
6	2, 3, 5	3bitri 297	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
7		eliun 4959	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})))
8		eldif 3924	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ))
9		opelxp 5674	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		df-br 5108	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ I )
11		vex 3451	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	11	ideq 5816	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ 𝑖 = 𝑗)
13	10, 12	bitr3i 277	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 = 𝑗)
14	13	necon3bbii 2972	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 ≠ 𝑗)
15	9, 14	anbi12i 628	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
16	8, 15	bitri 275	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
17	16	anbi2i 623	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
18	17	2exbii 1849	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
19		eldifi 4094	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → 𝑝 ∈ (𝐴 × 𝐵))
20		elxpi 5660	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
21		simpl 482	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
22	21	2eximi 1836	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
23	19, 20, 22	3syl 18	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	ancli 548	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
25		19.42vv 1957	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
26	24, 25	sylibr 234	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
27		ancom 460	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )))
28		eleq1 2816	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
29	28	adantl 481	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
30	29	pm5.32da 579	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
31	27, 30	bitrid 283	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
32	31	2exbidv 1924	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
33	26, 32	mpbid 232	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
34	28	biimpar 477	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
35	34	exlimivv 1932	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
36	33, 35	impbii 209	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
37		r19.42v 3169	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
38		simprl 770	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ {𝑦})
39		velsn 4605	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑦} ↔ 𝑖 = 𝑦)
40	38, 39	sylib 218	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 = 𝑦)
41		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ∈ 𝐴)
42	40, 41	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ 𝐴)
43		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ (𝐵 ∖ {𝑦}))
44	43	eldifad 3926	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ 𝐵)
45	43	eldifbd 3927	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ¬ 𝑗 ∈ {𝑦})
46		velsn 4605	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
47	46	necon3bbii 2972	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑗 ∈ {𝑦} ↔ 𝑗 ≠ 𝑦)
48	45, 47	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ≠ 𝑦)
49	48	necomd 2980	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ≠ 𝑗)
50	40, 49	eqnetrd 2992	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ≠ 𝑗)
51	42, 44, 50	jca31 514	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
52	51	adantll 714	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
53		sneq 4599	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
54	53	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
55	53	difeq2d 4089	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦}))
56	55	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑦})))
57	54, 56	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))))
58	57	cbvrexvw 3216	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
59	58	biimpi 216	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
60	52, 59	r19.29a 3141	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
61		simpll 766	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴)
62		vsnid 4627	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
63	62	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ {𝑖})
64		simplr 768	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐵)
65		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗)
66	65	necomd 2980	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ≠ 𝑖)
67		velsn 4605	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑖} ↔ 𝑗 = 𝑖)
68	67	necon3bbii 2972	. . . . . . . . . . 11 ⊢ (¬ 𝑗 ∈ {𝑖} ↔ 𝑗 ≠ 𝑖)
69	66, 68	sylibr 234	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ¬ 𝑗 ∈ {𝑖})
70	64, 69	eldifd 3925	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ (𝐵 ∖ {𝑖}))
71		sneq 4599	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
72	71	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
73	71	difeq2d 4089	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑖}))
74	73	eleq2d 2814	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑖})))
75	72, 74	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))))
76	75	rspcev 3588	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
77	61, 63, 70, 76	syl12anc 836	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
78	60, 77	impbii 209	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
79	78	anbi2i 623	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
80	37, 79	bitri 275	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
81	80	2exbii 1849	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
82	18, 36, 81	3bitr4i 303	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
83	6, 7, 82	3bitr4i 303	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
84	83	eqriv 2726	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2925  ∃wrex 3053   ∖ cdif 3911  {csn 4589  ⟨cop 4595  ∪ ciun 4955   class class class wbr 5107   I cid 5532   × cxp 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-iun 4957  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645

This theorem is referenced by:  tglnfn  28474