Theorem frgrusgr 30331

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3051  ∃!wreu 3340   ∖ cdif 3886   ⊆ wss 3889  {csn 4567  {cpr 4569  ‘cfv 6498  Vtxcvtx 29065  Edgcedg 29116  USGraphcusgr 29218   FriendGraph cfrgr 30328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-frgr 30329

This theorem is referenced by:  frgreu  30338  frcond3  30339  nfrgr2v  30342  3vfriswmgr  30348  2pthfrgrrn2  30353  2pthfrgr  30354  3cyclfrgrrn2  30357  3cyclfrgr  30358  n4cyclfrgr  30361  frgrnbnb  30363  vdgn0frgrv2  30365  vdgn1frgrv2  30366  frgrncvvdeqlem2  30370  frgrncvvdeqlem3  30371  frgrncvvdeqlem6  30374  frgrncvvdeqlem9  30377  frgrncvvdeq  30379  frgrwopreglem4a  30380  frgrwopreg  30393  frgrregorufrg  30396  frgr2wwlkeu  30397  frgr2wsp1  30400  frgr2wwlkeqm  30401  frrusgrord0lem  30409  frrusgrord0  30410  friendshipgt3  30468