Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  relop Structured version   Visualization version   GIF version

Theorem relop 5194
 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 5045 . 2 (Rel ⟨𝐴, 𝐵⟩ ↔ ⟨𝐴, 𝐵⟩ ⊆ (V × V))
2 dfss2 3557 . . . . 5 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
3 relop.1 . . . . . . . . . 10 𝐴 ∈ V
4 relop.2 . . . . . . . . . 10 𝐵 ∈ V
53, 4elop 4862 . . . . . . . . 9 (𝑧 ∈ ⟨𝐴, 𝐵⟩ ↔ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}))
6 elvv 5100 . . . . . . . . 9 (𝑧 ∈ (V × V) ↔ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)
75, 6imbi12i 339 . . . . . . . 8 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩))
8 jaob 818 . . . . . . . 8 (((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
97, 8bitri 263 . . . . . . 7 ((𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
109albii 1737 . . . . . 6 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ ∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
11 19.26 1786 . . . . . 6 (∀𝑧((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ (𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
1210, 11bitri 263 . . . . 5 (∀𝑧(𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
132, 12bitri 263 . . . 4 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)))
14 snex 4835 . . . . . . 7 {𝐴} ∈ V
15 eqeq1 2614 . . . . . . . 8 (𝑧 = {𝐴} → (𝑧 = {𝐴} ↔ {𝐴} = {𝐴}))
16 eqeq1 2614 . . . . . . . . . 10 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴} = ⟨𝑥, 𝑦⟩))
17 eqcom 2617 . . . . . . . . . . 11 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴})
18 vex 3176 . . . . . . . . . . . 12 𝑥 ∈ V
19 vex 3176 . . . . . . . . . . . 12 𝑦 ∈ V
2018, 19, 3opeqsn 4892 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ = {𝐴} ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2117, 20bitri 263 . . . . . . . . . 10 ({𝐴} = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥}))
2216, 21syl6bb 275 . . . . . . . . 9 (𝑧 = {𝐴} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑦𝐴 = {𝑥})))
23222exbidv 1839 . . . . . . . 8 (𝑧 = {𝐴} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
2415, 23imbi12d 333 . . . . . . 7 (𝑧 = {𝐴} → ((𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}))))
2514, 24spcv 3272 . . . . . 6 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
26 sneq 4135 . . . . . . . . 9 (𝑤 = 𝑥 → {𝑤} = {𝑥})
2726eqeq2d 2620 . . . . . . . 8 (𝑤 = 𝑥 → (𝐴 = {𝑤} ↔ 𝐴 = {𝑥}))
2827cbvexv 2263 . . . . . . 7 (∃𝑤 𝐴 = {𝑤} ↔ ∃𝑥 𝐴 = {𝑥})
29 ax6evr 1929 . . . . . . . . 9 𝑦 𝑥 = 𝑦
30 19.41v 1901 . . . . . . . . 9 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ (∃𝑦 𝑥 = 𝑦𝐴 = {𝑥}))
3129, 30mpbiran 955 . . . . . . . 8 (∃𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ 𝐴 = {𝑥})
3231exbii 1764 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ∃𝑥 𝐴 = {𝑥})
33 eqid 2610 . . . . . . . 8 {𝐴} = {𝐴}
3433a1bi 351 . . . . . . 7 (∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥}) ↔ ({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})))
3528, 32, 343bitr2ri 288 . . . . . 6 (({𝐴} = {𝐴} → ∃𝑥𝑦(𝑥 = 𝑦𝐴 = {𝑥})) ↔ ∃𝑤 𝐴 = {𝑤})
3625, 35sylib 207 . . . . 5 (∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑤 𝐴 = {𝑤})
37 eqid 2610 . . . . . 6 {𝐴, 𝐵} = {𝐴, 𝐵}
38 prex 4836 . . . . . . 7 {𝐴, 𝐵} ∈ V
39 eqeq1 2614 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (𝑧 = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐴, 𝐵}))
40 eqeq1 2614 . . . . . . . . 9 (𝑧 = {𝐴, 𝐵} → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ {𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
41402exbidv 1839 . . . . . . . 8 (𝑧 = {𝐴, 𝐵} → (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4239, 41imbi12d 333 . . . . . . 7 (𝑧 = {𝐴, 𝐵} → ((𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ↔ ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)))
4338, 42spcv 3272 . . . . . 6 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ({𝐴, 𝐵} = {𝐴, 𝐵} → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩))
4437, 43mpi 20 . . . . 5 (∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩)
45 eqcom 2617 . . . . . . . . . 10 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = {𝐴, 𝐵})
4618, 19, 3, 4opeqpr 4893 . . . . . . . . . 10 (⟨𝑥, 𝑦⟩ = {𝐴, 𝐵} ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
4745, 46bitri 263 . . . . . . . . 9 ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ ↔ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})))
48 idd 24 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
49 eqtr2 2630 . . . . . . . . . . . . . 14 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → {𝑥, 𝑦} = {𝑤})
50 vex 3176 . . . . . . . . . . . . . . . 16 𝑤 ∈ V
5118, 19, 50preqsn 4331 . . . . . . . . . . . . . . 15 ({𝑥, 𝑦} = {𝑤} ↔ (𝑥 = 𝑦𝑦 = 𝑤))
5251simplbi 475 . . . . . . . . . . . . . 14 ({𝑥, 𝑦} = {𝑤} → 𝑥 = 𝑦)
5349, 52syl 17 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → 𝑥 = 𝑦)
54 dfsn2 4138 . . . . . . . . . . . . . . . . . . . 20 {𝑥} = {𝑥, 𝑥}
55 preq2 4213 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → {𝑥, 𝑥} = {𝑥, 𝑦})
5654, 55syl5req 2657 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥, 𝑦} = {𝑥})
5756eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} ↔ 𝐴 = {𝑥}))
5854, 55syl5eq 2656 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → {𝑥} = {𝑥, 𝑦})
5958eqeq2d 2620 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → (𝐵 = {𝑥} ↔ 𝐵 = {𝑥, 𝑦}))
6057, 59anbi12d 743 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) ↔ (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6160biimpd 218 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑦 → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6261expd 451 . . . . . . . . . . . . . . 15 (𝑥 = 𝑦 → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6362com12 32 . . . . . . . . . . . . . 14 (𝐴 = {𝑥, 𝑦} → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6463adantr 480 . . . . . . . . . . . . 13 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝑥 = 𝑦 → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6553, 64mpd 15 . . . . . . . . . . . 12 ((𝐴 = {𝑥, 𝑦} ∧ 𝐴 = {𝑤}) → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6665expcom 450 . . . . . . . . . . 11 (𝐴 = {𝑤} → (𝐴 = {𝑥, 𝑦} → (𝐵 = {𝑥} → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))))
6766impd 446 . . . . . . . . . 10 (𝐴 = {𝑤} → ((𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥}) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6848, 67jaod 394 . . . . . . . . 9 (𝐴 = {𝑤} → (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∨ (𝐴 = {𝑥, 𝑦} ∧ 𝐵 = {𝑥})) → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
6947, 68syl5bi 231 . . . . . . . 8 (𝐴 = {𝑤} → ({𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → (𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
70692eximdv 1835 . . . . . . 7 (𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7170exlimiv 1845 . . . . . 6 (∃𝑤 𝐴 = {𝑤} → (∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦})))
7271imp 444 . . . . 5 ((∃𝑤 𝐴 = {𝑤} ∧ ∃𝑥𝑦{𝐴, 𝐵} = ⟨𝑥, 𝑦⟩) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7336, 44, 72syl2an 493 . . . 4 ((∀𝑧(𝑧 = {𝐴} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩) ∧ ∀𝑧(𝑧 = {𝐴, 𝐵} → ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩)) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
7413, 73sylbi 206 . . 3 (⟨𝐴, 𝐵⟩ ⊆ (V × V) → ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
75 simpr 476 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = {𝐴})
76 equid 1926 . . . . . . . . . . . . . 14 𝑥 = 𝑥
7776jctl 562 . . . . . . . . . . . . 13 (𝐴 = {𝑥} → (𝑥 = 𝑥𝐴 = {𝑥}))
7818, 18, 3opeqsn 4892 . . . . . . . . . . . . 13 (⟨𝑥, 𝑥⟩ = {𝐴} ↔ (𝑥 = 𝑥𝐴 = {𝑥}))
7977, 78sylibr 223 . . . . . . . . . . . 12 (𝐴 = {𝑥} → ⟨𝑥, 𝑥⟩ = {𝐴})
8079adantr 480 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ⟨𝑥, 𝑥⟩ = {𝐴})
8175, 80eqtr4d 2647 . . . . . . . . . 10 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → 𝑧 = ⟨𝑥, 𝑥⟩)
82 opeq12 4342 . . . . . . . . . . . 12 ((𝑤 = 𝑥𝑣 = 𝑥) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑥⟩)
8382eqeq2d 2620 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑥) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩))
8418, 18, 83spc2ev 3274 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑥⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
8581, 84syl 17 . . . . . . . . 9 ((𝐴 = {𝑥} ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
8685adantlr 747 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
87 preq12 4214 . . . . . . . . . . . 12 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → {𝐴, 𝐵} = {{𝑥}, {𝑥, 𝑦}})
8887eqeq2d 2620 . . . . . . . . . . 11 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 = {𝐴, 𝐵} ↔ 𝑧 = {{𝑥}, {𝑥, 𝑦}}))
8988biimpa 500 . . . . . . . . . 10 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = {{𝑥}, {𝑥, 𝑦}})
9018, 19dfop 4339 . . . . . . . . . 10 𝑥, 𝑦⟩ = {{𝑥}, {𝑥, 𝑦}}
9189, 90syl6eqr 2662 . . . . . . . . 9 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → 𝑧 = ⟨𝑥, 𝑦⟩)
92 opeq12 4342 . . . . . . . . . . 11 ((𝑤 = 𝑥𝑣 = 𝑦) → ⟨𝑤, 𝑣⟩ = ⟨𝑥, 𝑦⟩)
9392eqeq2d 2620 . . . . . . . . . 10 ((𝑤 = 𝑥𝑣 = 𝑦) → (𝑧 = ⟨𝑤, 𝑣⟩ ↔ 𝑧 = ⟨𝑥, 𝑦⟩))
9418, 19, 93spc2ev 3274 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9591, 94syl 17 . . . . . . . 8 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9686, 95jaodan 822 . . . . . . 7 (((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) ∧ (𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵})) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9796ex 449 . . . . . 6 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ((𝑧 = {𝐴} ∨ 𝑧 = {𝐴, 𝐵}) → ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩))
98 elvv 5100 . . . . . 6 (𝑧 ∈ (V × V) ↔ ∃𝑤𝑣 𝑧 = ⟨𝑤, 𝑣⟩)
9997, 5, 983imtr4g 284 . . . . 5 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → (𝑧 ∈ ⟨𝐴, 𝐵⟩ → 𝑧 ∈ (V × V)))
10099ssrdv 3574 . . . 4 ((𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
101100exlimivv 1847 . . 3 (∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}) → ⟨𝐴, 𝐵⟩ ⊆ (V × V))
10274, 101impbii 198 . 2 (⟨𝐴, 𝐵⟩ ⊆ (V × V) ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
1031, 102bitri 263 1 (Rel ⟨𝐴, 𝐵⟩ ↔ ∃𝑥𝑦(𝐴 = {𝑥} ∧ 𝐵 = {𝑥, 𝑦}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173   ⊆ wss 3540  {csn 4125  {cpr 4127  ⟨cop 4131   × cxp 5036  Rel wrel 5043 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-opab 4644  df-xp 5044  df-rel 5045 This theorem is referenced by:  funopg  5836
 Copyright terms: Public domain W3C validator