Theorem frgrusgr 30353

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

Syntax hints:   → wi 4   ∈ wcel 2121  ∀wral 3055  ∃!wreu 3344   ∖ cdif 3882   ⊆ wss 3885  {csn 4558  {cpr 4560  ‘cfv 6489  Vtxcvtx 29087  Edgcedg 29138  USGraphcusgr 29240   FriendGraph cfrgr 30350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-frgr 30351

This theorem is referenced by:  frgreu  30360  frcond3  30361  nfrgr2v  30364  3vfriswmgr  30370  2pthfrgrrn2  30375  2pthfrgr  30376  3cyclfrgrrn2  30379  3cyclfrgr  30380  n4cyclfrgr  30383  frgrnbnb  30385  vdgn0frgrv2  30387  vdgn1frgrv2  30388  frgrncvvdeqlem2  30392  frgrncvvdeqlem3  30393  frgrncvvdeqlem6  30396  frgrncvvdeqlem9  30399  frgrncvvdeq  30401  frgrwopreglem4a  30402  frgrwopreg  30415  frgrregorufrg  30418  frgr2wwlkeu  30419  frgr2wsp1  30422  frgr2wwlkeqm  30423  frrusgrord0lem  30431  frrusgrord0  30432  friendshipgt3  30490