Theorem frgrusgr 30240

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 30239	. 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 28976  Edgcedg 29027  USGraphcusgr 29129   FriendGraph cfrgr 30237

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 30238

This theorem is referenced by:  frgreu  30247  frcond3  30248  nfrgr2v  30251  3vfriswmgr  30257  2pthfrgrrn2  30262  2pthfrgr  30263  3cyclfrgrrn2  30266  3cyclfrgr  30267  n4cyclfrgr  30270  frgrnbnb  30272  vdgn0frgrv2  30274  vdgn1frgrv2  30275  frgrncvvdeqlem2  30279  frgrncvvdeqlem3  30280  frgrncvvdeqlem6  30283  frgrncvvdeqlem9  30286  frgrncvvdeq  30288  frgrwopreglem4a  30289  frgrwopreg  30302  frgrregorufrg  30305  frgr2wwlkeu  30306  frgr2wsp1  30309  frgr2wwlkeqm  30310  frrusgrord0lem  30318  frrusgrord0  30319  friendshipgt3  30377