Theorem frgrusgr 30163

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044  ∃!wreu 3349   ∖ cdif 3908   ⊆ wss 3911  {csn 4585  {cpr 4587  ‘cfv 6499  Vtxcvtx 28899  Edgcedg 28950  USGraphcusgr 29052   FriendGraph cfrgr 30160

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 5256

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 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-frgr 30161

This theorem is referenced by:  frgreu  30170  frcond3  30171  nfrgr2v  30174  3vfriswmgr  30180  2pthfrgrrn2  30185  2pthfrgr  30186  3cyclfrgrrn2  30189  3cyclfrgr  30190  n4cyclfrgr  30193  frgrnbnb  30195  vdgn0frgrv2  30197  vdgn1frgrv2  30198  frgrncvvdeqlem2  30202  frgrncvvdeqlem3  30203  frgrncvvdeqlem6  30206  frgrncvvdeqlem9  30209  frgrncvvdeq  30211  frgrwopreglem4a  30212  frgrwopreg  30225  frgrregorufrg  30228  frgr2wwlkeu  30229  frgr2wsp1  30232  frgr2wwlkeqm  30233  frrusgrord0lem  30241  frrusgrord0  30242  friendshipgt3  30300