Theorem xpdifcnvepel 6167

Description: The set of couples in a Cartesian product, where the second is not an element of the first. (Contributed by Thierry Arnoux, 17-Jun-2026.)

Assertion

Ref	Expression
xpdifcnvepel	⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) = ((𝐴 × 𝐵) ∖ ◡ E )

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem xpdifcnvepel

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

Step	Hyp	Ref	Expression
1		elxp 5685	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
2	1	rexbii 3118	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
3		rexcom4 3298	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
4		rexcom4 3298	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
5	4	exbii 1875	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
6	2, 3, 5	3bitri 300	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
7		eliun 4964	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)))
8		eldif 3923	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ))
9		opelxp 5698	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		vex 3467	. . . . . . . . . . 11 ⊢ 𝑖 ∈ V
11		vex 3467	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	10, 11	brcnv 5869	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ 𝑗 E 𝑖)
13		df-br 5114	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ ◡ E )
14		epel 5565	. . . . . . . . . 10 ⊢ (𝑗 E 𝑖 ↔ 𝑗 ∈ 𝑖)
15	12, 13, 14	3bitr3i 304	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ 𝑗 ∈ 𝑖)
16	15	notbii 323	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ ¬ 𝑗 ∈ 𝑖)
17	9, 16	anbi12i 639	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
18	8, 17	bitri 278	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
19	18	anbi2i 634	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
20	19	2exbii 1876	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
21		eldifi 4093	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → 𝑝 ∈ (𝐴 × 𝐵))
22		elxpi 5684	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
23		simpl 487	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	2eximi 1863	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
25	21, 22, 24	3syl 19	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
26	25	ancli 557	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
27		19.42vv 1984	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
28	26, 27	sylibr 237	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
29		ancom 465	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
30		eleq1 2857	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
31	30	adantl 486	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
32	31	pm5.32da 589	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
33	29, 32	bitrid 286	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
34	33	2exbidv 1951	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
35	28, 34	mpbid 235	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
36	30	biimpar 482	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
37	36	exlimivv 1959	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
38	35, 37	impbii 212	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
39		r19.42v 3203	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
40		simprl 782	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ {𝑦})
41	40	elsnd 4612	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 = 𝑦)
42		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑦 ∈ 𝐴)
43	41, 42	eqeltrd 2869	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ 𝐴)
44		simprr 784	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ (𝐵 ∖ 𝑦))
45	44	eldifad 3925	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ 𝐵)
46	44	eldifbd 3926	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑦)
47	46, 41	neleqtrrd 2892	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑖)
48	43, 45, 47	jca31 523	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
49	48	adantll 726	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
50		sneq 4604	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
51	50	eleq2d 2855	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
52		difeq2 4083	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑦))
53	52	eleq2d 2855	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑦)))
54	51, 53	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))))
55	54	cbvrexvw 3250	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
56	55	biimpi 219	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
57	49, 56	r19.29a 3179	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
58		simpll 778	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ 𝐴)
59		vsnid 4634	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
60	59	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ {𝑖})
61		simplr 780	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ 𝐵)
62		simpr 489	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ¬ 𝑗 ∈ 𝑖)
63	61, 62	eldifd 3924	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ (𝐵 ∖ 𝑖))
64		sneq 4604	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
65	64	eleq2d 2855	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
66		difeq2 4083	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑖))
67	66	eleq2d 2855	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑖)))
68	65, 67	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))))
69	68	rspcev 3590	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
70	58, 60, 63, 69	syl12anc 849	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
71	57, 70	impbii 212	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
72	71	anbi2i 634	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
73	39, 72	bitri 278	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
74	73	2exbii 1876	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
75	20, 38, 74	3bitr4i 306	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
76	6, 7, 75	3bitr4i 306	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
77	76	eqriv 2766	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) = ((𝐴 × 𝐵) ∖ ◡ E )

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095   ∖ cdif 3910  {csn 4594  ⟨cop 4600  ∪ ciun 4960   class class class wbr 5113   E cep 5561   × cxp 5660  ^◡ccnv 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-11 2198  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-iun 4962  df-br 5114  df-opab 5178  df-eprel 5562  df-xp 5668  df-cnv 5670

This theorem is referenced by:  tgplnfn  29014