Theorem frgrusgr 30280

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3061  ∃!wreu 3378   ∖ cdif 3948   ⊆ wss 3951  {csn 4626  {cpr 4628  ‘cfv 6561  Vtxcvtx 29013  Edgcedg 29064  USGraphcusgr 29166   FriendGraph cfrgr 30277

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-frgr 30278

This theorem is referenced by:  frgreu  30287  frcond3  30288  nfrgr2v  30291  3vfriswmgr  30297  2pthfrgrrn2  30302  2pthfrgr  30303  3cyclfrgrrn2  30306  3cyclfrgr  30307  n4cyclfrgr  30310  frgrnbnb  30312  vdgn0frgrv2  30314  vdgn1frgrv2  30315  frgrncvvdeqlem2  30319  frgrncvvdeqlem3  30320  frgrncvvdeqlem6  30323  frgrncvvdeqlem9  30326  frgrncvvdeq  30328  frgrwopreglem4a  30329  frgrwopreg  30342  frgrregorufrg  30345  frgr2wwlkeu  30346  frgr2wsp1  30349  frgr2wwlkeqm  30350  frrusgrord0lem  30358  frrusgrord0  30359  friendshipgt3  30417