Theorem frgrusgr 30197

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3045  ∃!wreu 3354   ∖ cdif 3914   ⊆ wss 3917  {csn 4592  {cpr 4594  ‘cfv 6514  Vtxcvtx 28930  Edgcedg 28981  USGraphcusgr 29083   FriendGraph cfrgr 30194

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 2702  ax-nul 5264

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-frgr 30195

This theorem is referenced by:  frgreu  30204  frcond3  30205  nfrgr2v  30208  3vfriswmgr  30214  2pthfrgrrn2  30219  2pthfrgr  30220  3cyclfrgrrn2  30223  3cyclfrgr  30224  n4cyclfrgr  30227  frgrnbnb  30229  vdgn0frgrv2  30231  vdgn1frgrv2  30232  frgrncvvdeqlem2  30236  frgrncvvdeqlem3  30237  frgrncvvdeqlem6  30240  frgrncvvdeqlem9  30243  frgrncvvdeq  30245  frgrwopreglem4a  30246  frgrwopreg  30259  frgrregorufrg  30262  frgr2wwlkeu  30263  frgr2wsp1  30266  frgr2wwlkeqm  30267  frrusgrord0lem  30275  frrusgrord0  30276  friendshipgt3  30334