Theorem frgrusgr 30205

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 2729	. . 3 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		eqid 2729	. . 3 ⊢ (Edg‘𝐺) = (Edg‘𝐺)
3	1, 2	isfrgr 30204	. 2 ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ (Vtx‘𝐺)∀𝑙 ∈ ((Vtx‘𝐺) ∖ {𝑘})∃!𝑥 ∈ (Vtx‘𝐺){{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ (Edg‘𝐺)))
4	3	simplbi 497	1 ⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph)

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044  ∃!wreu 3341   ∖ cdif 3900   ⊆ wss 3903  {csn 4577  {cpr 4579  ‘cfv 6482  Vtxcvtx 28941  Edgcedg 28992  USGraphcusgr 29094   FriendGraph cfrgr 30202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-frgr 30203

This theorem is referenced by:  frgreu  30212  frcond3  30213  nfrgr2v  30216  3vfriswmgr  30222  2pthfrgrrn2  30227  2pthfrgr  30228  3cyclfrgrrn2  30231  3cyclfrgr  30232  n4cyclfrgr  30235  frgrnbnb  30237  vdgn0frgrv2  30239  vdgn1frgrv2  30240  frgrncvvdeqlem2  30244  frgrncvvdeqlem3  30245  frgrncvvdeqlem6  30248  frgrncvvdeqlem9  30251  frgrncvvdeq  30253  frgrwopreglem4a  30254  frgrwopreg  30267  frgrregorufrg  30270  frgr2wwlkeu  30271  frgr2wsp1  30274  frgr2wwlkeqm  30275  frrusgrord0lem  30283  frrusgrord0  30284  friendshipgt3  30342