Theorem xpdifid 5992

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 5542	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
2	1	rexbii 3210	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
3		rexcom4 3212	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
4		rexcom4 3212	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
5	4	exbii 1849	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
6	2, 3, 5	3bitri 300	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
7		eliun 4885	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ {𝑥})))
8		eldif 3891	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ))
9		opelxp 5555	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		df-br 5031	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ I )
11		vex 3444	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	11	ideq 5687	. . . . . . . . . 10 ⊢ (𝑖 I 𝑗 ↔ 𝑖 = 𝑗)
13	10, 12	bitr3i 280	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 = 𝑗)
14	13	necon3bbii 3034	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ I ↔ 𝑖 ≠ 𝑗)
15	9, 14	anbi12i 629	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
16	8, 15	bitri 278	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
17	16	anbi2i 625	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
18	17	2exbii 1850	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
19		eldifi 4054	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → 𝑝 ∈ (𝐴 × 𝐵))
20		elxpi 5541	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
21		simpl 486	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
22	21	2eximi 1837	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
23	19, 20, 22	3syl 18	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	ancli 552	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
25		19.42vv 1958	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
26	24, 25	sylibr 237	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
27		ancom 464	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )))
28		eleq1 2877	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
29	28	adantl 485	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
30	29	pm5.32da 582	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
31	27, 30	syl5bb 286	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
32	31	2exbidv 1925	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I ))))
33	26, 32	mpbid 235	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
34	28	biimpar 481	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
35	34	exlimivv 1933	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
36	33, 35	impbii 212	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ I )))
37		r19.42v 3303	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
38		simprl 770	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ {𝑦})
39		velsn 4541	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ {𝑦} ↔ 𝑖 = 𝑦)
40	38, 39	sylib 221	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 = 𝑦)
41		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ∈ 𝐴)
42	40, 41	eqeltrd 2890	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ∈ 𝐴)
43		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ (𝐵 ∖ {𝑦}))
44	43	eldifad 3893	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ∈ 𝐵)
45	43	eldifbd 3894	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ¬ 𝑗 ∈ {𝑦})
46		velsn 4541	. . . . . . . . . . . . . . 15 ⊢ (𝑗 ∈ {𝑦} ↔ 𝑗 = 𝑦)
47	46	necon3bbii 3034	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑗 ∈ {𝑦} ↔ 𝑗 ≠ 𝑦)
48	45, 47	sylib 221	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑗 ≠ 𝑦)
49	48	necomd 3042	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑦 ≠ 𝑗)
50	40, 49	eqnetrd 3054	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → 𝑖 ≠ 𝑗)
51	42, 44, 50	jca31 518	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
52	51	adantll 713	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
53		sneq 4535	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
54	53	eleq2d 2875	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
55	53	difeq2d 4050	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑦}))
56	55	eleq2d 2875	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑦})))
57	54, 56	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦}))))
58	57	cbvrexvw 3397	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
59	58	biimpi 219	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ {𝑦})))
60	52, 59	r19.29a 3248	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
61		simpll 766	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ 𝐴)
62		vsnid 4562	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
63	62	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ∈ {𝑖})
64		simplr 768	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ 𝐵)
65		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑖 ≠ 𝑗)
66	65	necomd 3042	. . . . . . . . . . 11 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ≠ 𝑖)
67		velsn 4541	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ {𝑖} ↔ 𝑗 = 𝑖)
68	67	necon3bbii 3034	. . . . . . . . . . 11 ⊢ (¬ 𝑗 ∈ {𝑖} ↔ 𝑗 ≠ 𝑖)
69	66, 68	sylibr 237	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ¬ 𝑗 ∈ {𝑖})
70	64, 69	eldifd 3892	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → 𝑗 ∈ (𝐵 ∖ {𝑖}))
71		sneq 4535	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
72	71	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
73	71	difeq2d 4050	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ {𝑥}) = (𝐵 ∖ {𝑖}))
74	73	eleq2d 2875	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ {𝑥}) ↔ 𝑗 ∈ (𝐵 ∖ {𝑖})))
75	72, 74	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))))
76	75	rspcev 3571	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ {𝑖}))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
77	61, 63, 70, 76	syl12anc 835	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})))
78	60, 77	impbii 212	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥})) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗))
79	78	anbi2i 625	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
80	37, 79	bitri 278	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
81	80	2exbii 1850	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ 𝑖 ≠ 𝑗)))
82	18, 36, 81	3bitr4i 306	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ I ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ {𝑥}))))
83	6, 7, 82	3bitr4i 306	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ I ))
84	83	eqriv 2795	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ {𝑥})) = ((𝐴 × 𝐵) ∖ I )

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107   ∖ cdif 3878  {csn 4525  ⟨cop 4531  ∪ ciun 4881   class class class wbr 5030   I cid 5424   × cxp 5517

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-iun 4883  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526

This theorem is referenced by:  tglnfn  26341