![]() |
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 2733 | . . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺) | |
2 | eqid 2733 | . . 3 ⊢ (Edg‘𝐺) = (Edg‘𝐺) | |
3 | 1, 2 | isfrgr 29513 | . 2 ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺))) |
4 | 3 | simplbi 499 | 1 ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∀wral 3062 ∃!wreu 3375 ∖ cdif 3946 ⊆ wss 3949 {csn 4629 {cpr 4631 ‘cfv 6544 Vtxcvtx 28256 Edgcedg 28307 USGraphcusgr 28409 FriendGraph cfrgr 29511 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-nul 5307 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-frgr 29512 |
This theorem is referenced by: frgreu 29521 frcond3 29522 nfrgr2v 29525 3vfriswmgr 29531 2pthfrgrrn2 29536 2pthfrgr 29537 3cyclfrgrrn2 29540 3cyclfrgr 29541 n4cyclfrgr 29544 frgrnbnb 29546 vdgn0frgrv2 29548 vdgn1frgrv2 29549 frgrncvvdeqlem2 29553 frgrncvvdeqlem3 29554 frgrncvvdeqlem6 29557 frgrncvvdeqlem9 29560 frgrncvvdeq 29562 frgrwopreglem4a 29563 frgrwopreg 29576 frgrregorufrg 29579 frgr2wwlkeu 29580 frgr2wsp1 29583 frgr2wwlkeqm 29584 frrusgrord0lem 29592 frrusgrord0 29593 friendshipgt3 29651 |
Copyright terms: Public domain | W3C validator |