Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > frgrusgr | Structured version Visualization version GIF version |
Description: A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) |
Ref | Expression |
---|---|
frgrusgr | ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | eqid 2738 | . . 3 ⊢ (Edg‘𝐺) = (Edg‘𝐺) | |
3 | 1, 2 | isfrgr 28197 | . 2 ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
4 | 3 | simplbi 501 | 1 ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 ∀wral 3053 ∃!wreu 3055 ∖ cdif 3840 ⊆ wss 3843 {csn 4516 {cpr 4518 ‘cfv 6339 Vtxcvtx 26941 Edgcedg 26992 USGraphcusgr 27094 FriendGraph cfrgr 28195 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-nul 5174 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-ral 3058 df-rex 3059 df-reu 3060 df-rab 3062 df-v 3400 df-sbc 3681 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-br 5031 df-iota 6297 df-fv 6347 df-frgr 28196 |
This theorem is referenced by: frgreu 28205 frcond3 28206 nfrgr2v 28209 3vfriswmgr 28215 2pthfrgrrn2 28220 2pthfrgr 28221 3cyclfrgrrn2 28224 3cyclfrgr 28225 n4cyclfrgr 28228 frgrnbnb 28230 vdgn0frgrv2 28232 vdgn1frgrv2 28233 frgrncvvdeqlem2 28237 frgrncvvdeqlem3 28238 frgrncvvdeqlem6 28241 frgrncvvdeqlem9 28244 frgrncvvdeq 28246 frgrwopreglem4a 28247 frgrwopreg 28260 frgrregorufrg 28263 frgr2wwlkeu 28264 frgr2wsp1 28267 frgr2wwlkeqm 28268 frrusgrord0lem 28276 frrusgrord0 28277 friendshipgt3 28335 |
Copyright terms: Public domain | W3C validator |