Theorem xpdifid 5562

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 5131	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
2	1	rexbii 3041	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
3		rexcom4 3225	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
4		rexcom4 3225	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
5	4	exbii 1774	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
6	2, 3, 5	3bitri 286	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
7		eliun 4524	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})))
8		eldif 3584	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ))
9		opelxp 5146	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		df-br 4654	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ I )
11		vex 3203	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	11	ideq 5274	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ 𝑖 = 𝑗)
13	10, 12	bitr3i 266	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 = 𝑗)
14	13	necon3bbii 2841	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 ≠ 𝑗)
15	9, 14	anbi12i 733	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
16	8, 15	bitri 264	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
17	16	anbi2i 730	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
18	17	2exbii 1775	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
19		eldifi 3732	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → 𝑝 ∈ (𝐴 × 𝐵))
20		elxpi 5130	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
21		simpl 473	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
22	21	2eximi 1763	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
23	19, 20, 22	3syl 18	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	ancli 574	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
25		19.42vv 1920	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
26	24, 25	sylibr 224	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
27		ancom 466	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )))
28		eleq1 2689	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
29	28	adantl 482	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
30	29	pm5.32da 673	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
31	27, 30	syl5bb 272	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
32	31	2exbidv 1852	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
33	26, 32	mpbid 222	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
34	28	biimpar 502	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
35	34	exlimivv 1860	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
36	33, 35	impbii 199	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
37		r19.42v 3092	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
38		simprl 794	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ {𝑦})
39		velsn 4193	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑦} ↔ 𝑖 = 𝑦)
40	38, 39	sylib 208	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 = 𝑦)
41		simpl 473	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ∈ 𝐴)
42	40, 41	eqeltrd 2701	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ 𝐴)
43		simprr 796	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ (𝐵 ∖ {𝑦}))
44	43	eldifad 3586	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ 𝐵)
45	43	eldifbd 3587	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ¬ 𝑗 ∈ {𝑦})
46		velsn 4193	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
47	46	necon3bbii 2841	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑗 ∈ {𝑦} ↔ 𝑗 ≠ 𝑦)
48	45, 47	sylib 208	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ≠ 𝑦)
49	48	necomd 2849	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ≠ 𝑗)
50	40, 49	eqnetrd 2861	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ≠ 𝑗)
51	42, 44, 50	jca31 557	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
52	51	adantll 750	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
53		sneq 4187	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
54	53	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
55	53	difeq2d 3728	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦}))
56	55	eleq2d 2687	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑦})))
57	54, 56	anbi12d 747	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))))
58	57	cbvrexv 3172	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
59	58	biimpi 206	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
60	52, 59	r19.29a 3078	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
61		simpll 790	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴)
62		vsnid 4209	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
63	62	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ {𝑖})
64		simplr 792	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐵)
65		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗)
66	65	necomd 2849	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ≠ 𝑖)
67		velsn 4193	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑖} ↔ 𝑗 = 𝑖)
68	67	necon3bbii 2841	. . . . . . . . . . 11 ⊢ (¬ 𝑗 ∈ {𝑖} ↔ 𝑗 ≠ 𝑖)
69	66, 68	sylibr 224	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ¬ 𝑗 ∈ {𝑖})
70	64, 69	eldifd 3585	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ (𝐵 ∖ {𝑖}))
71		sneq 4187	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
72	71	eleq2d 2687	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
73	71	difeq2d 3728	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑖}))
74	73	eleq2d 2687	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑖})))
75	72, 74	anbi12d 747	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))))
76	75	rspcev 3309	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
77	61, 63, 70, 76	syl12anc 1324	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
78	60, 77	impbii 199	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
79	78	anbi2i 730	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
80	37, 79	bitri 264	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
81	80	2exbii 1775	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
82	18, 36, 81	3bitr4i 292	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
83	6, 7, 82	3bitr4i 292	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
84	83	eqriv 2619	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990   ≠ wne 2794  ∃wrex 2913   ∖ cdif 3571  {csn 4177  ⟨cop 4183  ∪ ciun 4520   class class class wbr 4653   I cid 5023   × cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-iun 4522  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121

This theorem is referenced by:  tglnfn  25442