![]() |
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 29493 | . 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 3944 ⊆ wss 3947 {csn 4627 {cpr 4629 ‘cfv 6540 Vtxcvtx 28236 Edgcedg 28287 USGraphcusgr 28389 FriendGraph cfrgr 29491 |
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 5305 |
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 3777 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-iota 6492 df-fv 6548 df-frgr 29492 |
This theorem is referenced by: frgreu 29501 frcond3 29502 nfrgr2v 29505 3vfriswmgr 29511 2pthfrgrrn2 29516 2pthfrgr 29517 3cyclfrgrrn2 29520 3cyclfrgr 29521 n4cyclfrgr 29524 frgrnbnb 29526 vdgn0frgrv2 29528 vdgn1frgrv2 29529 frgrncvvdeqlem2 29533 frgrncvvdeqlem3 29534 frgrncvvdeqlem6 29537 frgrncvvdeqlem9 29540 frgrncvvdeq 29542 frgrwopreglem4a 29543 frgrwopreg 29556 frgrregorufrg 29559 frgr2wwlkeu 29560 frgr2wsp1 29563 frgr2wwlkeqm 29564 frrusgrord0lem 29572 frrusgrord0 29573 friendshipgt3 29631 |
Copyright terms: Public domain | W3C validator |