Theorem frgrusgr 29511

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3061  ∃!wreu 3374   ∖ cdif 3945   ⊆ wss 3948  {csn 4628  {cpr 4630  ‘cfv 6543  Vtxcvtx 28253  Edgcedg 28304  USGraphcusgr 28406   FriendGraph cfrgr 29508

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-frgr 29509

This theorem is referenced by:  frgreu  29518  frcond3  29519  nfrgr2v  29522  3vfriswmgr  29528  2pthfrgrrn2  29533  2pthfrgr  29534  3cyclfrgrrn2  29537  3cyclfrgr  29538  n4cyclfrgr  29541  frgrnbnb  29543  vdgn0frgrv2  29545  vdgn1frgrv2  29546  frgrncvvdeqlem2  29550  frgrncvvdeqlem3  29551  frgrncvvdeqlem6  29554  frgrncvvdeqlem9  29557  frgrncvvdeq  29559  frgrwopreglem4a  29560  frgrwopreg  29573  frgrregorufrg  29576  frgr2wwlkeu  29577  frgr2wsp1  29580  frgr2wwlkeqm  29581  frrusgrord0lem  29589  frrusgrord0  29590  friendshipgt3  29648