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

Theorem relop 4753
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 4610 . 2 (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2 dfss2 3130 . . . . 5 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3 vex 2728 . . . . . . . . . 10 𝑧 ∈ V
4 relop.1 . . . . . . . . . 10 𝐴 ∈ V
5 relop.2 . . . . . . . . . 10 𝐵 ∈ V
63, 4, 5elop 4208 . . . . . . . . 9 (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
7 elvv 4665 . . . . . . . . 9 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
86, 7imbi12i 238 . . . . . . . 8 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
9 jaob 700 . . . . . . . 8 (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
108, 9bitri 183 . . . . . . 7 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1110albii 1458 . . . . . 6 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
12 19.26 1469 . . . . . 6 (∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1311, 12bitri 183 . . . . 5 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
142, 13bitri 183 . . . 4 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
154snex 4163 . . . . . . 7 {𝐴} ∈ V
16 eqeq1 2172 . . . . . . . 8 (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
17 eqeq1 2172 . . . . . . . . . 10 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
18 eqcom 2167 . . . . . . . . . . 11 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
19 vex 2728 . . . . . . . . . . . 12 𝑥 ∈ V
20 vex 2728 . . . . . . . . . . . 12 𝑦 ∈ V
2119, 20, 4opeqsn 4229 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2218, 21bitri 183 . . . . . . . . . 10 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2317, 22bitrdi 195 . . . . . . . . 9 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥})))
24232exbidv 1856 . . . . . . . 8 (𝑧 = {𝐴} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
2516, 24imbi12d 233 . . . . . . 7 (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}))))
2615, 25spcv 2819 . . . . . 6 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
27 sneq 3586 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤} = {𝑥})
2827eqeq2d 2177 . . . . . . . 8 (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
2928cbvexv 1906 . . . . . . 7 (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
30 a9ev 1685 . . . . . . . . . 10 𝑦 𝑦 = 𝑥
31 equcom 1694 . . . . . . . . . . 11 (𝑦 = 𝑥𝑥 = 𝑦)
3231exbii 1593 . . . . . . . . . 10 (∃𝑦 𝑦 = 𝑥 ↔ ∃𝑦 𝑥 = 𝑦)
3330, 32mpbi 144 . . . . . . . . 9 𝑦 𝑥 = 𝑦
34 19.41v 1890 . . . . . . . . 9 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦𝐴 = {𝑥}))
3533, 34mpbiran 930 . . . . . . . 8 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
3635exbii 1593 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
37 eqid 2165 . . . . . . . 8 {𝐴} = {𝐴}
3837a1bi 242 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
3929, 36, 383bitr2ri 208 . . . . . 6 (({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
4026, 39sylib 121 . . . . 5 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
41 eqid 2165 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵}
42 prexg 4188 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
434, 5, 42mp2an 423 . . . . . . 7 {𝐴, 𝐵} ∈ V
44 eqeq1 2172 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
45 eqeq1 2172 . . . . . . . . 9 (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
46452exbidv 1856 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4744, 46imbi12d 233 . . . . . . 7 (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
4843, 47spcv 2819 . . . . . 6 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4941, 48mpi 15 . . . . 5 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
50 eqcom 2167 . . . . . . . . . 10 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
5119, 20, 4, 5opeqpr 4230 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
5250, 51bitri 183 . . . . . . . . 9 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
53 idd 21 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
54 eqtr2 2184 . . . . . . . . . . . . . 14 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
55 vex 2728 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5619, 20, 55preqsn 3754 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦𝑦 = 𝑤))
5756simplbi 272 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
5854, 57syl 14 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
59 dfsn2 3589 . . . . . . . . . . . . . . . . . . . 20 {𝑥} = {𝑥, 𝑥}
60 preq2 3653 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
6159, 60eqtr2id 2211 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
6261eqeq2d 2177 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
6359, 60syl5eq 2210 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
6463eqeq2d 2177 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
6562, 64anbi12d 465 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6665biimpd 143 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6766expd 256 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6867com12 30 . . . . . . . . . . . . . 14 (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6968adantr 274 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7058, 69mpd 13 . . . . . . . . . . . 12 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7170expcom 115 . . . . . . . . . . 11 (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7271impd 252 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7353, 72jaod 707 . . . . . . . . 9 (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7452, 73syl5bi 151 . . . . . . . 8 (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
75742eximdv 1870 . . . . . . 7 (𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7675exlimiv 1586 . . . . . 6 (∃𝑤 𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7776imp 123 . . . . 5 ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7840, 49, 77syl2an 287 . . . 4 ((∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7914, 78sylbi 120 . . 3 (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
80 simpr 109 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
81 equid 1689 . . . . . . . . . . . . . 14 𝑥 = 𝑥
8281jctl 312 . . . . . . . . . . . . 13 (𝐴 = {𝑥} → (𝑥 = 𝑥𝐴 = {𝑥}))
8319, 19, 4opeqsn 4229 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥𝐴 = {𝑥}))
8482, 83sylibr 133 . . . . . . . . . . . 12 (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
8584adantr 274 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
8680, 85eqtr4d 2201 . . . . . . . . . 10 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
87 opeq12 3759 . . . . . . . . . . . 12 ((𝑤 = 𝑥𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
8887eqeq2d 2177 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
8919, 19, 88spc2ev 2821 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9086, 89syl 14 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9190adantlr 469 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
92 preq12 3654 . . . . . . . . . . . 12 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
9392eqeq2d 2177 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
9493biimpa 294 . . . . . . . . . 10 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
9519, 20dfop 3756 . . . . . . . . . 10 𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
9694, 95eqtr4di 2216 . . . . . . . . 9 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
97 opeq12 3759 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
9897eqeq2d 2177 . . . . . . . . . 10 ((𝑤 = 𝑥𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
9919, 20, 98spc2ev 2821 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10096, 99syl 14 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10191, 100jaodan 787 . . . . . . 7 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
102101ex 114 . . . . . 6 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
103 elvv 4665 . . . . . 6 (𝑧 ∈ (V × V) ↔ ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
104102, 6, 1033imtr4g 204 . . . . 5 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
105104ssrdv 3147 . . . 4 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
106105exlimivv 1884 . . 3 (∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
10779, 106impbii 125 . 2 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
1081, 107bitri 183 1 (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wo 698  wal 1341   = wceq 1343  wex 1480  wcel 2136  Vcvv 2725  wss 3115  {csn 3575  {cpr 3576  cop 3578   × cxp 4601  Rel wrel 4608
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4099  ax-pow 4152  ax-pr 4186
This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-un 3119  df-in 3121  df-ss 3128  df-pw 3560  df-sn 3581  df-pr 3582  df-op 3584  df-opab 4043  df-xp 4609  df-rel 4610
This theorem is referenced by:  funopg  5221
  Copyright terms: Public domain W3C validator