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

Theorem relop 4599
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 4459 . 2 (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2 dfss2 3015 . . . . 5 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3 vex 2623 . . . . . . . . . 10 𝑧 ∈ V
4 relop.1 . . . . . . . . . 10 𝐴 ∈ V
5 relop.2 . . . . . . . . . 10 𝐵 ∈ V
63, 4, 5elop 4067 . . . . . . . . 9 (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
7 elvv 4513 . . . . . . . . 9 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
86, 7imbi12i 238 . . . . . . . 8 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
9 jaob 667 . . . . . . . 8 (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
108, 9bitri 183 . . . . . . 7 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1110albii 1405 . . . . . 6 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
12 19.26 1416 . . . . . 6 (∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1311, 12bitri 183 . . . . 5 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
142, 13bitri 183 . . . 4 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
154snex 4026 . . . . . . 7 {𝐴} ∈ V
16 eqeq1 2095 . . . . . . . 8 (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
17 eqeq1 2095 . . . . . . . . . 10 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
18 eqcom 2091 . . . . . . . . . . 11 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
19 vex 2623 . . . . . . . . . . . 12 𝑥 ∈ V
20 vex 2623 . . . . . . . . . . . 12 𝑦 ∈ V
2119, 20, 4opeqsn 4088 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2218, 21bitri 183 . . . . . . . . . 10 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2317, 22syl6bb 195 . . . . . . . . 9 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥})))
24232exbidv 1797 . . . . . . . 8 (𝑧 = {𝐴} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
2516, 24imbi12d 233 . . . . . . 7 (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}))))
2615, 25spcv 2713 . . . . . 6 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
27 sneq 3461 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤} = {𝑥})
2827eqeq2d 2100 . . . . . . . 8 (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
2928cbvexv 1844 . . . . . . 7 (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
30 a9ev 1633 . . . . . . . . . 10 𝑦 𝑦 = 𝑥
31 equcom 1640 . . . . . . . . . . 11 (𝑦 = 𝑥𝑥 = 𝑦)
3231exbii 1542 . . . . . . . . . 10 (∃𝑦 𝑦 = 𝑥 ↔ ∃𝑦 𝑥 = 𝑦)
3330, 32mpbi 144 . . . . . . . . 9 𝑦 𝑥 = 𝑦
34 19.41v 1831 . . . . . . . . 9 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦𝐴 = {𝑥}))
3533, 34mpbiran 887 . . . . . . . 8 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
3635exbii 1542 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
37 eqid 2089 . . . . . . . 8 {𝐴} = {𝐴}
3837a1bi 242 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
3929, 36, 383bitr2ri 208 . . . . . 6 (({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
4026, 39sylib 121 . . . . 5 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
41 eqid 2089 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵}
42 prexg 4047 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → {𝐴, 𝐵} ∈ V)
434, 5, 42mp2an 418 . . . . . . 7 {𝐴, 𝐵} ∈ V
44 eqeq1 2095 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
45 eqeq1 2095 . . . . . . . . 9 (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
46452exbidv 1797 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4744, 46imbi12d 233 . . . . . . 7 (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
4843, 47spcv 2713 . . . . . 6 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4941, 48mpi 15 . . . . 5 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
50 eqcom 2091 . . . . . . . . . 10 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
5119, 20, 4, 5opeqpr 4089 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
5250, 51bitri 183 . . . . . . . . 9 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
53 idd 21 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
54 eqtr2 2107 . . . . . . . . . . . . . 14 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
55 vex 2623 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5619, 20, 55preqsn 3625 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦𝑦 = 𝑤))
5756simplbi 269 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
5854, 57syl 14 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
59 dfsn2 3464 . . . . . . . . . . . . . . . . . . . 20 {𝑥} = {𝑥, 𝑥}
60 preq2 3524 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
6159, 60syl5req 2134 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
6261eqeq2d 2100 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
6359, 60syl5eq 2133 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
6463eqeq2d 2100 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
6562, 64anbi12d 458 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6665biimpd 143 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6766expd 255 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6867com12 30 . . . . . . . . . . . . . 14 (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6968adantr 271 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7058, 69mpd 13 . . . . . . . . . . . 12 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7170expcom 115 . . . . . . . . . . 11 (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
7271impd 252 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7353, 72jaod 673 . . . . . . . . 9 (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7452, 73syl5bi 151 . . . . . . . 8 (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
75742eximdv 1811 . . . . . . 7 (𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7675exlimiv 1535 . . . . . 6 (∃𝑤 𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7776imp 123 . . . . 5 ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7840, 49, 77syl2an 284 . . . 4 ((∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7914, 78sylbi 120 . . 3 (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
80 simpr 109 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
81 equid 1635 . . . . . . . . . . . . . 14 𝑥 = 𝑥
8281jctl 308 . . . . . . . . . . . . 13 (𝐴 = {𝑥} → (𝑥 = 𝑥𝐴 = {𝑥}))
8319, 19, 4opeqsn 4088 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥𝐴 = {𝑥}))
8482, 83sylibr 133 . . . . . . . . . . . 12 (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
8584adantr 271 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
8680, 85eqtr4d 2124 . . . . . . . . . 10 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
87 opeq12 3630 . . . . . . . . . . . 12 ((𝑤 = 𝑥𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
8887eqeq2d 2100 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
8919, 19, 88spc2ev 2715 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9086, 89syl 14 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9190adantlr 462 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
92 preq12 3525 . . . . . . . . . . . 12 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
9392eqeq2d 2100 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
9493biimpa 291 . . . . . . . . . 10 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
9519, 20dfop 3627 . . . . . . . . . 10 𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
9694, 95syl6eqr 2139 . . . . . . . . 9 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
97 opeq12 3630 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
9897eqeq2d 2100 . . . . . . . . . 10 ((𝑤 = 𝑥𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
9919, 20, 98spc2ev 2715 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10096, 99syl 14 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
10191, 100jaodan 747 . . . . . . 7 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
102101ex 114 . . . . . 6 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
103 elvv 4513 . . . . . 6 (𝑧 ∈ (V × V) ↔ ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
104102, 6, 1033imtr4g 204 . . . . 5 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
105104ssrdv 3032 . . . 4 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
106105exlimivv 1825 . . 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 665  wal 1288   = wceq 1290  wex 1427  wcel 1439  Vcvv 2620  wss 3000  {csn 3450  {cpr 3451  cop 3453   × cxp 4450  Rel wrel 4457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015  ax-pr 4045
This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-un 3004  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456  df-pr 3457  df-op 3459  df-opab 3906  df-xp 4458  df-rel 4459
This theorem is referenced by:  funopg  5061
  Copyright terms: Public domain W3C validator