Theorem xpdifcnvepel 6154

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 5670	. . . . 5 ⊢ (𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
2	1	rexbii 3109	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
3		rexcom4 3289	. . . 4 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
4		rexcom4 3289	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
5	4	exbii 1868	. . . 4 ⊢ (∃𝑖∃𝑥 ∈ 𝐴 ∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
6	2, 3, 5	3bitri 299	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
7		eliun 4953	. . 3 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ ∃𝑥 ∈ 𝐴 𝑝 ∈ ({𝑥} × (𝐵 ∖ 𝑥)))
8		eldif 3914	. . . . . . 7 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ))
9		opelxp 5683	. . . . . . . 8 ⊢ (⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ↔ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵))
10		vex 3458	. . . . . . . . . . 11 ⊢ 𝑖 ∈ V
11		vex 3458	. . . . . . . . . . 11 ⊢ 𝑗 ∈ V
12	10, 11	brcnv 5854	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ 𝑗 E 𝑖)
13		df-br 5101	. . . . . . . . . 10 ⊢ (𝑖◡ E 𝑗 ↔ ⟨𝑖, 𝑗⟩ ∈ ◡ E )
14		epel 5550	. . . . . . . . . 10 ⊢ (𝑗 E 𝑖 ↔ 𝑗 ∈ 𝑖)
15	12, 13, 14	3bitr3i 303	. . . . . . . . 9 ⊢ (⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ 𝑗 ∈ 𝑖)
16	15	notbii 322	. . . . . . . 8 ⊢ (¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ↔ ¬ 𝑗 ∈ 𝑖)
17	9, 16	anbi12i 637	. . . . . . 7 ⊢ ((⟨𝑖, 𝑗⟩ ∈ (𝐴 × 𝐵) ∧ ¬ ⟨𝑖, 𝑗⟩ ∈ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
18	8, 17	bitri 277	. . . . . 6 ⊢ (⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
19	18	anbi2i 632	. . . . 5 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
20	19	2exbii 1869	. . . 4 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
21		eldifi 4084	. . . . . . . . 9 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → 𝑝 ∈ (𝐴 × 𝐵))
22		elxpi 5669	. . . . . . . . 9 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)))
23		simpl 486	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → 𝑝 = ⟨𝑖, 𝑗⟩)
24	23	2eximi 1856	. . . . . . . . 9 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵)) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
25	21, 22, 24	3syl 18	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩)
26	25	ancli 556	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
27		19.42vv 1977	. . . . . . 7 ⊢ (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ ∃𝑖∃𝑗 𝑝 = ⟨𝑖, 𝑗⟩))
28	26, 27	sylibr 236	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩))
29		ancom 464	. . . . . . . 8 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
30		eleq1 2850	. . . . . . . . . 10 ⊢ (𝑝 = ⟨𝑖, 𝑗⟩ → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
31	30	adantl 485	. . . . . . . . 9 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) → (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
32	31	pm5.32da 587	. . . . . . . 8 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E )) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
33	29, 32	bitrid 285	. . . . . . 7 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ((𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
34	33	2exbidv 1944	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → (∃𝑖∃𝑗(𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ∧ 𝑝 = ⟨𝑖, 𝑗⟩) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E ))))
35	28, 34	mpbid 234	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) → ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
36	30	biimpar 481	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
37	36	exlimivv 1952	. . . . 5 ⊢ (∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )) → 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
38	35, 37	impbii 211	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ⟨𝑖, 𝑗⟩ ∈ ((𝐴 × 𝐵) ∖ ◡ E )))
39		r19.42v 3194	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
40		simprl 780	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ {𝑦})
41	40	elsnd 4600	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 = 𝑦)
42		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑦 ∈ 𝐴)
43	41, 42	eqeltrd 2862	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑖 ∈ 𝐴)
44		simprr 782	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ (𝐵 ∖ 𝑦))
45	44	eldifad 3916	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → 𝑗 ∈ 𝐵)
46	44	eldifbd 3917	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑦)
47	46, 41	neleqtrrd 2885	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ¬ 𝑗 ∈ 𝑖)
48	43, 45, 47	jca31 522	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
49	48	adantll 724	. . . . . . . . 9 ⊢ (((∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ∧ 𝑦 ∈ 𝐴) ∧ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
50		sneq 4592	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦})
51	50	eleq2d 2848	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑦}))
52		difeq2 4074	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑦))
53	52	eleq2d 2848	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑦)))
54	51, 53	anbi12d 641	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦))))
55	54	cbvrexvw 3241	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
56	55	biimpi 218	. . . . . . . . 9 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ∃𝑦 ∈ 𝐴 (𝑖 ∈ {𝑦} ∧ 𝑗 ∈ (𝐵 ∖ 𝑦)))
57	49, 56	r19.29a 3170	. . . . . . . 8 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
58		simpll 776	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ 𝐴)
59		vsnid 4622	. . . . . . . . . 10 ⊢ 𝑖 ∈ {𝑖}
60	59	a1i 11	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑖 ∈ {𝑖})
61		simplr 778	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ 𝐵)
62		simpr 488	. . . . . . . . . 10 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ¬ 𝑗 ∈ 𝑖)
63	61, 62	eldifd 3915	. . . . . . . . 9 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → 𝑗 ∈ (𝐵 ∖ 𝑖))
64		sneq 4592	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → {𝑥} = {𝑖})
65	64	eleq2d 2848	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑖 ∈ {𝑥} ↔ 𝑖 ∈ {𝑖}))
66		difeq2 4074	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑖 → (𝐵 ∖ 𝑥) = (𝐵 ∖ 𝑖))
67	66	eleq2d 2848	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ (𝐵 ∖ 𝑥) ↔ 𝑗 ∈ (𝐵 ∖ 𝑖)))
68	65, 67	anbi12d 641	. . . . . . . . . 10 ⊢ (𝑥 = 𝑖 → ((𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))))
69	68	rspcev 3581	. . . . . . . . 9 ⊢ ((𝑖 ∈ 𝐴 ∧ (𝑖 ∈ {𝑖} ∧ 𝑗 ∈ (𝐵 ∖ 𝑖))) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
70	58, 60, 63, 69	syl12anc 847	. . . . . . . 8 ⊢ (((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖) → ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)))
71	57, 70	impbii 211	. . . . . . 7 ⊢ (∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥)) ↔ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖))
72	71	anbi2i 632	. . . . . 6 ⊢ ((𝑝 = ⟨𝑖, 𝑗⟩ ∧ ∃𝑥 ∈ 𝐴 (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
73	39, 72	bitri 277	. . . . 5 ⊢ (∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ (𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
74	73	2exbii 1869	. . . 4 ⊢ (∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))) ↔ ∃𝑖∃𝑗(𝑝 = ⟨𝑖, 𝑗⟩ ∧ ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵) ∧ ¬ 𝑗 ∈ 𝑖)))
75	20, 38, 74	3bitr4i 305	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ) ↔ ∃𝑖∃𝑗∃𝑥 ∈ 𝐴 (𝑝 = ⟨𝑖, 𝑗⟩ ∧ (𝑖 ∈ {𝑥} ∧ 𝑗 ∈ (𝐵 ∖ 𝑥))))
76	6, 7, 75	3bitr4i 305	. 2 ⊢ (𝑝 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) ↔ 𝑝 ∈ ((𝐴 × 𝐵) ∖ ◡ E ))
77	76	eqriv 2759	1 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐵 ∖ 𝑥)) = ((𝐴 × 𝐵) ∖ ◡ E )

Syntax hints:  ¬ wn 3   ↔ wb 208   ∧ wa 399   = wceq 1560  ∃wex 1799   ∈ wcel 2142  ∃wrex 3086   ∖ cdif 3901  {csn 4582  ⟨cop 4588  ∪ ciun 4949   class class class wbr 5100   E cep 5546   × cxp 5645  ^◡ccnv 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-11 2191  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-iun 4951  df-br 5101  df-opab 5163  df-eprel 5547  df-xp 5653  df-cnv 5655

This theorem is referenced by:  tgplnfn  28979