ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  relop GIF version

Theorem relop 4789
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.
StepHypRef Expression
1 df-rel 4645 . 2 (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2 dfss2 3156 . . . . 5 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3 vex 2752 . . . . . . . . . 10 𝑧 ∈ V
4 relop.1 . . . . . . . . . 10 𝐴 ∈ V
5 relop.2 . . . . . . . . . 10 𝐵 ∈ V
63, 4, 5elop 4243 . . . . . . . . 9 (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
7 elvv 4700 . . . . . . . . 9 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
86, 7imbi12i 239 . . . . . . . 8 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
9 jaob 711 . . . . . . . 8 (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
108, 9bitri 184 . . . . . . 7 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1110albii 1480 . . . . . 6 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
12 19.26 1491 . . . . . 6 (∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1311, 12bitri 184 . . . . 5 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
142, 13bitri 184 . . . 4 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
154snex 4197 . . . . . . 7 {𝐴} ∈ V
16 eqeq1 2194 . . . . . . . 8 (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
17 eqeq1 2194 . . . . . . . . . 10 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
18 eqcom 2189 . . . . . . . . . . 11 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
19 vex 2752 . . . . . . . . . . . 12 𝑥 ∈ V
20 vex 2752 . . . . . . . . . . . 12 𝑦 ∈ V
2119, 20, 4opeqsn 4264 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2218, 21bitri 184 . . . . . . . . . 10 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2317, 22bitrdi 196 . . . . . . . . 9 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥})))
24232exbidv 1878 . . . . . . . 8 (𝑧 = {𝐴} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
2516, 24imbi12d 234 . . . . . . 7 (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}))))
2615, 25spcv 2843 . . . . . 6 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
27 sneq 3615 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤} = {𝑥})
2827eqeq2d 2199 . . . . . . . 8 (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
2928cbvexv 1928 . . . . . . 7 (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
30 a9ev 1707 . . . . . . . . . 10 𝑦 𝑦 = 𝑥
31 equcom 1716 . . . . . . . . . . 11 (𝑦 = 𝑥𝑥 = 𝑦)
3231exbii 1615 . . . . . . . . . 10 (∃𝑦 𝑦 = 𝑥 ↔ ∃𝑦 𝑥 = 𝑦)
3330, 32mpbi 145 . . . . . . . . 9 𝑦 𝑥 = 𝑦
34 19.41v 1912 . . . . . . . . 9 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦𝐴 = {𝑥}))
3533, 34mpbiran 941 . . . . . . . 8 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
3635exbii 1615 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
37 eqid 2187 . . . . . . . 8 {𝐴} = {𝐴}
3837a1bi 243 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
3929, 36, 383bitr2ri 209 . . . . . 6 (({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
4026, 39sylib 122 . . . . 5 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
41 eqid 2187 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵}
42 prexg 4223 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
434, 5, 42mp2an 426 . . . . . . 7 {𝐴, 𝐵} ∈ V
44 eqeq1 2194 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
45 eqeq1 2194 . . . . . . . . 9 (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
46452exbidv 1878 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4744, 46imbi12d 234 . . . . . . 7 (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
4843, 47spcv 2843 . . . . . 6 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4941, 48mpi 15 . . . . 5 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
50 eqcom 2189 . . . . . . . . . 10 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
5119, 20, 4, 5opeqpr 4265 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
5250, 51bitri 184 . . . . . . . . 9 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
53 idd 21 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
54 eqtr2 2206 . . . . . . . . . . . . . 14 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
55 vex 2752 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5619, 20, 55preqsn 3787 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦𝑦 = 𝑤))
5756simplbi 274 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
5854, 57syl 14 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
59 dfsn2 3618 . . . . . . . . . . . . . . . . . . . 20 {𝑥} = {𝑥, 𝑥}
60 preq2 3682 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
6159, 60eqtr2id 2233 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
6261eqeq2d 2199 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
6359, 60eqtrid 2232 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
6463eqeq2d 2199 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
6562, 64anbi12d 473 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6665biimpd 144 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6766expd 258 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6867com12 30 . . . . . . . . . . . . . 14 (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6968adantr 276 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7058, 69mpd 13 . . . . . . . . . . . 12 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7170expcom 116 . . . . . . . . . . 11 (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7271impd 254 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7353, 72jaod 718 . . . . . . . . 9 (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7452, 73biimtrid 152 . . . . . . . 8 (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
75742eximdv 1892 . . . . . . 7 (𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7675exlimiv 1608 . . . . . 6 (∃𝑤 𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7776imp 124 . . . . 5 ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7840, 49, 77syl2an 289 . . . 4 ((∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7914, 78sylbi 121 . . 3 (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
80 simpr 110 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
81 equid 1711 . . . . . . . . . . . . . 14 𝑥 = 𝑥
8281jctl 314 . . . . . . . . . . . . 13 (𝐴 = {𝑥} → (𝑥 = 𝑥𝐴 = {𝑥}))
8319, 19, 4opeqsn 4264 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥𝐴 = {𝑥}))
8482, 83sylibr 134 . . . . . . . . . . . 12 (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
8584adantr 276 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
8680, 85eqtr4d 2223 . . . . . . . . . 10 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
87 opeq12 3792 . . . . . . . . . . . 12 ((𝑤 = 𝑥𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
8887eqeq2d 2199 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
8919, 19, 88spc2ev 2845 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9086, 89syl 14 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9190adantlr 477 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
92 preq12 3683 . . . . . . . . . . . 12 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
9392eqeq2d 2199 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
9493biimpa 296 . . . . . . . . . 10 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
9519, 20dfop 3789 . . . . . . . . . 10 𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
9694, 95eqtr4di 2238 . . . . . . . . 9 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
97 opeq12 3792 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
9897eqeq2d 2199 . . . . . . . . . 10 ((𝑤 = 𝑥𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
9919, 20, 98spc2ev 2845 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10096, 99syl 14 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10191, 100jaodan 798 . . . . . . 7 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
102101ex 115 . . . . . 6 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
103 elvv 4700 . . . . . 6 (𝑧 ∈ (V × V) ↔ ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
104102, 6, 1033imtr4g 205 . . . . 5 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
105104ssrdv 3173 . . . 4 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
106105exlimivv 1906 . . 3 (∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
10779, 106impbii 126 . 2 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
1081, 107bitri 184 1 (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wo 709  wal 1361   = wceq 1363  wex 1502  wcel 2158  Vcvv 2749  wss 3141  {csn 3604  {cpr 3605  cop 3607   × cxp 4636  Rel wrel 4643
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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-opab 4077  df-xp 4644  df-rel 4645
This theorem is referenced by:  funopg  5262
  Copyright terms: Public domain W3C validator