Theorem relop 4816

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) (Avoid depending on this detail.)

Hypotheses

Ref	Expression
relop.1	⊢ 𝐴 ∈ V
relop.2	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
relop	⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem relop

Dummy variables 𝑤 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rel 4670	. 2 ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2		dfss2 3172	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3		vex 2766	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
4		relop.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ V
5		relop.2	. . . . . . . . . 10 ⊢ 𝐵 ∈ V
6	3, 4, 5	elop 4264	. . . . . . . . 9 ⊢ (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
7		elvv 4725	. . . . . . . . 9 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
8	6, 7	imbi12i 239	. . . . . . . 8 ⊢ ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
9		jaob 711	. . . . . . . 8 ⊢ (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
10	8, 9	bitri 184	. . . . . . 7 ⊢ ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
11	10	albii 1484	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
12		19.26 1495	. . . . . 6 ⊢ (∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
13	11, 12	bitri 184	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
14	2, 13	bitri 184	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
15	4	snex 4218	. . . . . . 7 ⊢ {𝐴} ∈ V
16		eqeq1 2203	. . . . . . . 8 ⊢ (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
17		eqeq1 2203	. . . . . . . . . 10 ⊢ (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
18		eqcom 2198	. . . . . . . . . . 11 ⊢ ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
19		vex 2766	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
20		vex 2766	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
21	19, 20, 4	opeqsn 4285	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
22	18, 21	bitri 184	. . . . . . . . . 10 ⊢ ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
23	17, 22	bitrdi 196	. . . . . . . . 9 ⊢ (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
24	23	2exbidv 1882	. . . . . . . 8 ⊢ (𝑧 = {𝐴} → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
25	16, 24	imbi12d 234	. . . . . . 7 ⊢ (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))))
26	15, 25	spcv 2858	. . . . . 6 ⊢ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
27		sneq 3633	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → {𝑤} = {𝑥})
28	27	eqeq2d 2208	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
29	28	cbvexv 1933	. . . . . . 7 ⊢ (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
30		a9ev 1711	. . . . . . . . . 10 ⊢ ∃𝑦 𝑦 = 𝑥
31		equcom 1720	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
32	31	exbii 1619	. . . . . . . . . 10 ⊢ (∃𝑦 𝑦 = 𝑥 ↔ ∃𝑦 𝑥 = 𝑦)
33	30, 32	mpbi 145	. . . . . . . . 9 ⊢ ∃𝑦 𝑥 = 𝑦
34		19.41v 1917	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
35	33, 34	mpbiran 942	. . . . . . . 8 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
36	35	exbii 1619	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
37		eqid 2196	. . . . . . . 8 ⊢ {𝐴} = {𝐴}
38	37	a1bi 243	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
39	29, 36, 38	3bitr2ri 209	. . . . . 6 ⊢ (({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
40	26, 39	sylib 122	. . . . 5 ⊢ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
41		eqid 2196	. . . . . 6 ⊢ {𝐴, 𝐵} = {𝐴, 𝐵}
42		prexg 4244	. . . . . . . 8 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
43	4, 5, 42	mp2an 426	. . . . . . 7 ⊢ {𝐴, 𝐵} ∈ V
44		eqeq1 2203	. . . . . . . 8 ⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
45		eqeq1 2203	. . . . . . . . 9 ⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
46	45	2exbidv 1882	. . . . . . . 8 ⊢ (𝑧 = {𝐴, 𝐵} → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
47	44, 46	imbi12d 234	. . . . . . 7 ⊢ (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
48	43, 47	spcv 2858	. . . . . 6 ⊢ (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
49	41, 48	mpi 15	. . . . 5 ⊢ (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
50		eqcom 2198	. . . . . . . . . 10 ⊢ ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
51	19, 20, 4, 5	opeqpr 4286	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
52	50, 51	bitri 184	. . . . . . . . 9 ⊢ ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
53		idd 21	. . . . . . . . . 10 ⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
54		eqtr2 2215	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
55		vex 2766	. . . . . . . . . . . . . . . 16 ⊢ 𝑤 ∈ V
56	19, 20, 55	preqsn 3805	. . . . . . . . . . . . . . 15 ⊢ ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦 ∧ 𝑦 = 𝑤))
57	56	simplbi 274	. . . . . . . . . . . . . 14 ⊢ ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
58	54, 57	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
59		dfsn2 3636	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑥} = {𝑥, 𝑥}
60		preq2 3700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
61	59, 60	eqtr2id 2242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
62	61	eqeq2d 2208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
63	59, 60	eqtrid 2241	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
64	63	eqeq2d 2208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
65	62, 64	anbi12d 473	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
66	65	biimpd 144	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
67	66	expd 258	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
68	67	com12 30	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
69	68	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
70	58, 69	mpd 13	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
71	70	expcom 116	. . . . . . . . . . 11 ⊢ (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
72	71	impd 254	. . . . . . . . . 10 ⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
73	53, 72	jaod 718	. . . . . . . . 9 ⊢ (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
74	52, 73	biimtrid 152	. . . . . . . 8 ⊢ (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
75	74	2eximdv 1896	. . . . . . 7 ⊢ (𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
76	75	exlimiv 1612	. . . . . 6 ⊢ (∃𝑤 𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
77	76	imp 124	. . . . 5 ⊢ ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
78	40, 49, 77	syl2an 289	. . . 4 ⊢ ((∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
79	14, 78	sylbi 121	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
80		simpr 110	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
81		equid 1715	. . . . . . . . . . . . . 14 ⊢ 𝑥 = 𝑥
82	81	jctl 314	. . . . . . . . . . . . 13 ⊢ (𝐴 = {𝑥} → (𝑥 = 𝑥 ∧ 𝐴 = {𝑥}))
83	19, 19, 4	opeqsn 4285	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥 ∧ 𝐴 = {𝑥}))
84	82, 83	sylibr 134	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
85	84	adantr 276	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
86	80, 85	eqtr4d 2232	. . . . . . . . . 10 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
87		opeq12 3810	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
88	87	eqeq2d 2208	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
89	19, 19, 88	spc2ev 2860	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
90	86, 89	syl 14	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
91	90	adantlr 477	. . . . . . . 8 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
92		preq12 3701	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
93	92	eqeq2d 2208	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
94	93	biimpa 296	. . . . . . . . . 10 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
95	19, 20	dfop 3807	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
96	94, 95	eqtr4di 2247	. . . . . . . . 9 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
97		opeq12 3810	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
98	97	eqeq2d 2208	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
99	19, 20, 98	spc2ev 2860	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
100	96, 99	syl 14	. . . . . . . 8 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
101	91, 100	jaodan 798	. . . . . . 7 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
102	101	ex 115	. . . . . 6 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
103		elvv 4725	. . . . . 6 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
104	102, 6, 103	3imtr4g 205	. . . . 5 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
105	104	ssrdv 3189	. . . 4 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
106	105	exlimivv 1911	. . 3 ⊢ (∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
107	79, 106	impbii 126	. 2 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
108	1, 107	bitri 184	1 ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  ∀wal 1362   = wceq 1364  ∃wex 1506   ∈ wcel 2167  Vcvv 2763   ⊆ wss 3157  {csn 3622  {cpr 3623  ⟨cop 3625   × cxp 4661  Rel wrel 4668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-opab 4095  df-xp 4669  df-rel 4670

This theorem is referenced by:  funopg  5292