Theorem frgrusgr 29781

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∀wral 3059  ∃!wreu 3372   ∖ cdif 3944   ⊆ wss 3947  {csn 4627  {cpr 4629  ‘cfv 6542  Vtxcvtx 28523  Edgcedg 28574  USGraphcusgr 28676   FriendGraph cfrgr 29778

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fv 6550  df-frgr 29779

This theorem is referenced by:  frgreu  29788  frcond3  29789  nfrgr2v  29792  3vfriswmgr  29798  2pthfrgrrn2  29803  2pthfrgr  29804  3cyclfrgrrn2  29807  3cyclfrgr  29808  n4cyclfrgr  29811  frgrnbnb  29813  vdgn0frgrv2  29815  vdgn1frgrv2  29816  frgrncvvdeqlem2  29820  frgrncvvdeqlem3  29821  frgrncvvdeqlem6  29824  frgrncvvdeqlem9  29827  frgrncvvdeq  29829  frgrwopreglem4a  29830  frgrwopreg  29843  frgrregorufrg  29846  frgr2wwlkeu  29847  frgr2wsp1  29850  frgr2wwlkeqm  29851  frrusgrord0lem  29859  frrusgrord0  29860  friendshipgt3  29918