Theorem frgrusgr 30349

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052  ∃!wreu 3341   ∖ cdif 3887   ⊆ wss 3890  {csn 4568  {cpr 4570  ‘cfv 6493  Vtxcvtx 29082  Edgcedg 29133  USGraphcusgr 29235   FriendGraph cfrgr 30346

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-frgr 30347

This theorem is referenced by:  frgreu  30356  frcond3  30357  nfrgr2v  30360  3vfriswmgr  30366  2pthfrgrrn2  30371  2pthfrgr  30372  3cyclfrgrrn2  30375  3cyclfrgr  30376  n4cyclfrgr  30379  frgrnbnb  30381  vdgn0frgrv2  30383  vdgn1frgrv2  30384  frgrncvvdeqlem2  30388  frgrncvvdeqlem3  30389  frgrncvvdeqlem6  30392  frgrncvvdeqlem9  30395  frgrncvvdeq  30397  frgrwopreglem4a  30398  frgrwopreg  30411  frgrregorufrg  30414  frgr2wwlkeu  30415  frgr2wsp1  30418  frgr2wwlkeqm  30419  frrusgrord0lem  30427  frrusgrord0  30428  friendshipgt3  30486