Theorem xpdifcnvepel 6160

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 5674	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
2	1	rexbii 3110	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
3		rexcom4 3290	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
4		rexcom4 3290	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
5	4	exbii 1881	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
6	2, 3, 5	3bitri 300	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
7		eliun 4955	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)))
8		eldif 3909	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ))
9		opelxp 5687	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		vex 3455	. . . . . . . . . . 11 ⊢ 𝑖 ∈ V
11		vex 3455	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	10, 11	brcnv 5860	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ 𝑗 E 𝑖)
13		df-br 5104	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ ◡ E )
14		epel 5554	. . . . . . . . . 10 ⊢ (𝑗 E 𝑖 ↔ 𝑗 ∈ 𝑖)
15	12, 13, 14	3bitr3i 304	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ 𝑗 ∈ 𝑖)
16	15	notbii 323	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ ¬ 𝑗 ∈ 𝑖)
17	9, 16	anbi12i 640	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
18	8, 17	bitri 278	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
19	18	anbi2i 635	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
20	19	2exbii 1882	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
21		eldifi 4078	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → 𝑝 ∈ (𝐴 × 𝐵))
22		elxpi 5673	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
23		simpl 488	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	2eximi 1869	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
25	21, 22, 24	3syl 19	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
26	25	ancli 558	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
27		19.42vv 1990	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
28	26, 27	sylibr 237	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
29		ancom 466	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
30		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
31	30	adantl 487	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
32	31	pm5.32da 590	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
33	29, 32	bitrid 286	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
34	33	2exbidv 1957	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
35	28, 34	mpbid 235	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
36	30	biimpar 483	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
37	36	exlimivv 1965	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
38	35, 37	impbii 212	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
39		r19.42v 3195	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
40		simprl 783	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ {𝑦})
41	40	elsnd 4602	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 = 𝑦)
42		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑦 ∈ 𝐴)
43	41, 42	eqeltrd 2861	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ 𝐴)
44		simprr 785	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ (𝐵 ∖ 𝑦))
45	44	eldifad 3911	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ 𝐵)
46	44	eldifbd 3912	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑦)
47	46, 41	neleqtrrd 2884	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑖)
48	43, 45, 47	jca31 524	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
49	48	adantll 727	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
50		sneq 4594	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
51	50	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
52		difeq2 4068	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑦))
53	52	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑦)))
54	51, 53	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))))
55	54	cbvrexvw 3242	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
56	55	biimpi 219	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
57	49, 56	r19.29a 3171	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
58		simpll 779	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ 𝐴)
59		vsnid 4624	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
60	59	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ {𝑖})
61		simplr 781	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ 𝐵)
62		simpr 490	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ¬ 𝑗 ∈ 𝑖)
63	61, 62	eldifd 3910	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ (𝐵 ∖ 𝑖))
64		sneq 4594	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
65	64	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
66		difeq2 4068	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑖))
67	66	eleq2d 2847	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑖)))
68	65, 67	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))))
69	68	rspcev 3577	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
70	58, 60, 63, 69	syl12anc 850	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
71	57, 70	impbii 212	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
72	71	anbi2i 635	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
73	39, 72	bitri 278	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
74	73	2exbii 1882	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
75	20, 38, 74	3bitr4i 306	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
76	6, 7, 75	3bitr4i 306	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
77	76	eqriv 2758	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) = ((𝐴 × 𝐵) ∖ ◡ E )

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087   ∖ cdif 3896  {csn 4584  ⟨cop 4590  ∪ ciun 4951   class class class wbr 5103   E cep 5550   × cxp 5649  ^◡ccnv 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-11 2194  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-iun 4953  df-br 5104  df-opab 5168  df-eprel 5551  df-xp 5657  df-cnv 5659

This theorem is used by:  tgplnfn  29246