Theorem relop 5759

Description: A necessary and sufficient condition for a Kuratowski ordered pair to be a relation. (Contributed by NM, 3-Jun-2008.) A relation is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a relation is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is relsnopg 5713, as funsng 6485 is to funop 7021. (New usage is discouraged.)

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 5596	. 2 ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2		dfss2 3907	. . . . 5 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3		relop.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ V
4		relop.2	. . . . . . . . . 10 ⊢ 𝐵 ∈ V
5	3, 4	elop 5382	. . . . . . . . 9 ⊢ (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
6		elvv 5661	. . . . . . . . 9 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
7	5, 6	imbi12i 351	. . . . . . . 8 ⊢ ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
8		jaob 959	. . . . . . . 8 ⊢ (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
9	7, 8	bitri 274	. . . . . . 7 ⊢ ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
10	9	albii 1822	. . . . . 6 ⊢ (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
11		19.26 1873	. . . . . 6 ⊢ (∀𝑧((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
12	10, 11	bitri 274	. . . . 5 ⊢ (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
13	2, 12	bitri 274	. . . 4 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
14		snex 5354	. . . . . . 7 ⊢ {𝐴} ∈ V
15		eqeq1 2742	. . . . . . . 8 ⊢ (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
16		eqeq1 2742	. . . . . . . . . 10 ⊢ (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
17		eqcom 2745	. . . . . . . . . . 11 ⊢ ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
18		vex 3436	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
19		vex 3436	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
20	18, 19	opeqsn 5418	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
21	17, 20	bitri 274	. . . . . . . . . 10 ⊢ ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
22	16, 21	bitrdi 287	. . . . . . . . 9 ⊢ (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
23	22	2exbidv 1927	. . . . . . . 8 ⊢ (𝑧 = {𝐴} → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
24	15, 23	imbi12d 345	. . . . . . 7 ⊢ (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))))
25	14, 24	spcv 3544	. . . . . 6 ⊢ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
26		sneq 4571	. . . . . . . . 9 ⊢ (𝑤 = 𝑥 → {𝑤} = {𝑥})
27	26	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
28	27	cbvexvw 2040	. . . . . . 7 ⊢ (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
29		ax6evr 2018	. . . . . . . . 9 ⊢ ∃𝑦 𝑥 = 𝑦
30		19.41v 1953	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦 ∧ 𝐴 = {𝑥}))
31	29, 30	mpbiran 706	. . . . . . . 8 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
32	31	exbii 1850	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
33		eqid 2738	. . . . . . . 8 ⊢ {𝐴} = {𝐴}
34	33	a1bi 363	. . . . . . 7 ⊢ (∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})))
35	28, 32, 34	3bitr2ri 300	. . . . . 6 ⊢ (({𝐴} = {𝐴} → ∃𝑥∃𝑦(𝑥 = 𝑦 ∧ 𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
36	25, 35	sylib 217	. . . . 5 ⊢ (∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
37		eqid 2738	. . . . . 6 ⊢ {𝐴, 𝐵} = {𝐴, 𝐵}
38		prex 5355	. . . . . . 7 ⊢ {𝐴, 𝐵} ∈ V
39		eqeq1 2742	. . . . . . . 8 ⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
40		eqeq1 2742	. . . . . . . . 9 ⊢ (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
41	40	2exbidv 1927	. . . . . . . 8 ⊢ (𝑧 = {𝐴, 𝐵} → (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
42	39, 41	imbi12d 345	. . . . . . 7 ⊢ (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
43	38, 42	spcv 3544	. . . . . 6 ⊢ (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
44	37, 43	mpi 20	. . . . 5 ⊢ (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
45		eqcom 2745	. . . . . . . . . 10 ⊢ ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
46	18, 19, 3, 4	opeqpr 5419	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
47	45, 46	bitri 274	. . . . . . . . 9 ⊢ ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
48		idd 24	. . . . . . . . . 10 ⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
49		eqtr2 2762	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
50	18, 19	preqsn 4792	. . . . . . . . . . . . . . 15 ⊢ ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦 ∧ 𝑦 = 𝑤))
51	50	simplbi 498	. . . . . . . . . . . . . 14 ⊢ ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
52	49, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
53		dfsn2 4574	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑥} = {𝑥, 𝑥}
54		preq2 4670	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
55	53, 54	eqtr2id 2791	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
56	55	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
57	53, 54	eqtrid 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
58	57	eqeq2d 2749	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
59	56, 58	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
60	59	biimpd 228	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
61	60	expd 416	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
62	61	com12 32	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
63	62	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
64	52, 63	mpd 15	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
65	64	expcom 414	. . . . . . . . . . 11 ⊢ (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
66	65	impd 411	. . . . . . . . . 10 ⊢ (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
67	48, 66	jaod 856	. . . . . . . . 9 ⊢ (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
68	47, 67	syl5bi 241	. . . . . . . 8 ⊢ (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
69	68	2eximdv 1922	. . . . . . 7 ⊢ (𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
70	69	exlimiv 1933	. . . . . 6 ⊢ (∃𝑤 𝐴 = {𝑤} → (∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
71	70	imp 407	. . . . 5 ⊢ ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥∃𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
72	36, 44, 71	syl2an 596	. . . 4 ⊢ ((∀𝑧(𝑧 = {𝐴} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
73	13, 72	sylbi 216	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
74		simpr 485	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
75		equid 2015	. . . . . . . . . . . . . 14 ⊢ 𝑥 = 𝑥
76	75	jctl 524	. . . . . . . . . . . . 13 ⊢ (𝐴 = {𝑥} → (𝑥 = 𝑥 ∧ 𝐴 = {𝑥}))
77	18, 18	opeqsn 5418	. . . . . . . . . . . . 13 ⊢ (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥 ∧ 𝐴 = {𝑥}))
78	76, 77	sylibr 233	. . . . . . . . . . . 12 ⊢ (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
79	78	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
80	74, 79	eqtr4d 2781	. . . . . . . . . 10 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
81		opeq12 4806	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
82	81	eqeq2d 2749	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
83	18, 18, 82	spc2ev 3546	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
84	80, 83	syl 17	. . . . . . . . 9 ⊢ ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
85	84	adantlr 712	. . . . . . . 8 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
86		preq12 4671	. . . . . . . . . . . 12 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
87	86	eqeq2d 2749	. . . . . . . . . . 11 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
88	87	biimpa 477	. . . . . . . . . 10 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
89	18, 19	dfop 4803	. . . . . . . . . 10 ⊢ ⟨𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
90	88, 89	eqtr4di 2796	. . . . . . . . 9 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
91		opeq12 4806	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
92	91	eqeq2d 2749	. . . . . . . . . 10 ⊢ ((𝑤 = 𝑥 ∧ 𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
93	18, 19, 92	spc2ev 3546	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
94	90, 93	syl 17	. . . . . . . 8 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
95	85, 94	jaodan 955	. . . . . . 7 ⊢ (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
96	95	ex 413	. . . . . 6 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
97		elvv 5661	. . . . . 6 ⊢ (𝑧 ∈ (V × V) ↔ ∃𝑤∃𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
98	96, 5, 97	3imtr4g 296	. . . . 5 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
99	98	ssrdv 3927	. . . 4 ⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
100	99	exlimivv 1935	. . 3 ⊢ (∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
101	73, 100	impbii 208	. 2 ⊢ (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
102	1, 101	bitri 274	1 ⊢ (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥∃𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   ⊆ wss 3887  {csn 4561  {cpr 4563  ⟨cop 4567   × cxp 5587  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595  df-rel 5596

This theorem is referenced by:  funopg  6468