Theorem frgrusgr 30289

Description: A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)

Assertion

Ref	Expression
frgrusgr	⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph)

Proof of Theorem frgrusgr

Dummy variables 𝑘 𝑙 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2734	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2734	. . 3 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
3	1, 2	isfrgr 30288	. 2 ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)))
4	3	simplbi 497	1 ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph)

Syntax hints:   → wi 4   ∈ wcel 2105  ∀wral 3058  ∃!wreu 3375   ∖ cdif 3959   ⊆ wss 3962  {csn 4630  {cpr 4632  ‘cfv 6562  Vtxcvtx 29027  Edgcedg 29078  USGraphcusgr 29180   FriendGraph cfrgr 30286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-frgr 30287

This theorem is referenced by:  frgreu  30296  frcond3  30297  nfrgr2v  30300  3vfriswmgr  30306  2pthfrgrrn2  30311  2pthfrgr  30312  3cyclfrgrrn2  30315  3cyclfrgr  30316  n4cyclfrgr  30319  frgrnbnb  30321  vdgn0frgrv2  30323  vdgn1frgrv2  30324  frgrncvvdeqlem2  30328  frgrncvvdeqlem3  30329  frgrncvvdeqlem6  30332  frgrncvvdeqlem9  30335  frgrncvvdeq  30337  frgrwopreglem4a  30338  frgrwopreg  30351  frgrregorufrg  30354  frgr2wwlkeu  30355  frgr2wsp1  30358  frgr2wwlkeqm  30359  frrusgrord0lem  30367  frrusgrord0  30368  friendshipgt3  30426