Theorem xpdifcnvepel 6158

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 5675	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
2	1	rexbii 3112	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
3		rexcom4 3292	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
4		rexcom4 3292	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
5	4	exbii 1871	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
6	2, 3, 5	3bitri 300	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
7		eliun 4956	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)))
8		eldif 3917	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ))
9		opelxp 5688	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		vex 3461	. . . . . . . . . . 11 ⊢ 𝑖 ∈ V
11		vex 3461	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	10, 11	brcnv 5859	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ 𝑗 E 𝑖)
13		df-br 5106	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ ◡ E )
14		epel 5555	. . . . . . . . . 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 1872	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
21		eldifi 4087	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → 𝑝 ∈ (𝐴 × 𝐵))
22		elxpi 5674	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
23		simpl 487	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	2eximi 1859	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
25	21, 22, 24	3syl 19	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
26	25	ancli 557	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
27		19.42vv 1980	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
28	26, 27	sylibr 237	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
29		ancom 465	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
30		eleq1 2853	. . . . . . . . . 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 1947	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
35	28, 34	mpbid 235	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
36	30	biimpar 482	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
37	36	exlimivv 1955	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
38	35, 37	impbii 212	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
39		r19.42v 3197	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
40		simprl 782	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ {𝑦})
41	40	elsnd 4603	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 = 𝑦)
42		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑦 ∈ 𝐴)
43	41, 42	eqeltrd 2865	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ 𝐴)
44		simprr 784	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ (𝐵 ∖ 𝑦))
45	44	eldifad 3919	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ 𝐵)
46	44	eldifbd 3920	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑦)
47	46, 41	neleqtrrd 2888	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑖)
48	43, 45, 47	jca31 523	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
49	48	adantll 726	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
50		sneq 4595	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
51	50	eleq2d 2851	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
52		difeq2 4077	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑦))
53	52	eleq2d 2851	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑦)))
54	51, 53	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))))
55	54	cbvrexvw 3244	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
56	55	biimpi 219	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
57	49, 56	r19.29a 3173	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
58		simpll 778	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ 𝐴)
59		vsnid 4625	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
60	59	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ {𝑖})
61		simplr 780	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ 𝐵)
62		simpr 489	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ¬ 𝑗 ∈ 𝑖)
63	61, 62	eldifd 3918	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ (𝐵 ∖ 𝑖))
64		sneq 4595	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
65	64	eleq2d 2851	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
66		difeq2 4077	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑖))
67	66	eleq2d 2851	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑖)))
68	65, 67	anbi12d 643	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))))
69	68	rspcev 3584	. . . . . . . . 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 1872	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
75	20, 38, 74	3bitr4i 306	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
76	6, 7, 75	3bitr4i 306	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
77	76	eqriv 2762	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) = ((𝐴 × 𝐵) ∖ ◡ E )

Syntax hints:  ¬ wn 3   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089   ∖ cdif 3904  {csn 4585  ⟨cop 4591  ∪ ciun 4952   class class class wbr 5105   E cep 5551   × cxp 5650  ^◡ccnv 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-iun 4954  df-br 5106  df-opab 5168  df-eprel 5552  df-xp 5658  df-cnv 5660

This theorem is referenced by:  tgplnfn  29005