Theorem frgrusgr 28046

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106  ∃!wreu 3108   ∖ cdif 3878   ⊆ wss 3881  {csn 4525  {cpr 4527  ‘cfv 6324  Vtxcvtx 26789  Edgcedg 26840  USGraphcusgr 26942   FriendGraph cfrgr 28043

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-frgr 28044

This theorem is referenced by:  frgreu  28053  frcond3  28054  nfrgr2v  28057  3vfriswmgr  28063  2pthfrgrrn2  28068  2pthfrgr  28069  3cyclfrgrrn2  28072  3cyclfrgr  28073  n4cyclfrgr  28076  frgrnbnb  28078  vdgn0frgrv2  28080  vdgn1frgrv2  28081  frgrncvvdeqlem2  28085  frgrncvvdeqlem3  28086  frgrncvvdeqlem6  28089  frgrncvvdeqlem9  28092  frgrncvvdeq  28094  frgrwopreglem4a  28095  frgrwopreg  28108  frgrregorufrg  28111  frgr2wwlkeu  28112  frgr2wsp1  28115  frgr2wwlkeqm  28116  frrusgrord0lem  28124  frrusgrord0  28125  friendshipgt3  28183