Theorem frgrusgr 30460

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

Syntax hints:   → wi 4   ∈ wcel 2142  ∀wral 3076  ∃!wreu 3365   ∖ cdif 3901   ⊆ wss 3904  {csn 4582  {cpr 4584  ‘cfv 6521  Vtxcvtx 29194  Edgcedg 29245  USGraphcusgr 29347   FriendGraph cfrgr 30457

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-frgr 30458

This theorem is referenced by:  frgreu  30467  frcond3  30468  nfrgr2v  30471  3vfriswmgr  30477  2pthfrgrrn2  30482  2pthfrgr  30483  3cyclfrgrrn2  30486  3cyclfrgr  30487  n4cyclfrgr  30490  frgrnbnb  30492  vdgn0frgrv2  30494  vdgn1frgrv2  30495  frgrncvvdeqlem2  30499  frgrncvvdeqlem3  30500  frgrncvvdeqlem6  30503  frgrncvvdeqlem9  30506  frgrncvvdeq  30508  frgrwopreglem4a  30509  frgrwopreg  30522  frgrregorufrg  30525  frgr2wwlkeu  30526  frgr2wsp1  30529  frgr2wwlkeqm  30530  frrusgrord0lem  30538  frrusgrord0  30539  friendshipgt3  30597