MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frisusgra Structured version   Unicode version

Theorem frisusgra 25113
Description: A friendship graph is an undirected simple graph without loops. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
Assertion
Ref Expression
frisusgra  |-  ( V FriendGrph  E  ->  V USGrph  E )

Proof of Theorem frisusgra
Dummy variables  k 
l  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frisusgrapr 25112 . 2  |-  ( V FriendGrph  E  ->  ( V USGrph  E  /\  A. k  e.  V  A. l  e.  ( V  \  { k } ) E! x  e.  V  { { x ,  k } ,  { x ,  l } }  C_  ran  E ) )
21simpld 457 1  |-  ( V FriendGrph  E  ->  V USGrph  E )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wral 2732   E!wreu 2734    \ cdif 3386    C_ wss 3389   {csn 3944   {cpr 3946   class class class wbr 4367   ran crn 4914   USGrph cusg 24451   FriendGrph cfrgra 25109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-cnv 4921  df-dm 4923  df-rn 4924  df-frgra 25110
This theorem is referenced by:  frgra0v  25114  frgra2v  25120  3vfriswmgra  25126  2pthfrgrarn2  25131  2pthfrgra  25132  3cyclfrgrarn  25134  3cyclfrgrarn2  25135  3cyclfrgra  25136  n4cyclfrgra  25139  frgranbnb  25141  frconngra  25142  vdfrgra0  25143  vdn0frgrav2  25144  vdgn0frgrav2  25145  vdn1frgrav2  25146  vdgn1frgrav2  25147  vdgfrgragt2  25148  frgrancvvdeqlem2  25152  frgrancvvdeqlem3  25153  frgrancvvdeqlem4  25154  frgrancvvdeqlem7  25157  frgrancvvdeqlemC  25160  frgrancvvdeq  25163  frgrancvvdgeq  25164  frgrawopreglem1  25165  frgrawopreglem2  25166  frgrawopreglem4  25168  frgrawopreg  25170  frgraeu  25175  frg2woteu  25176  frg2wot1  25178  frg2spot1  25179  frg2woteqm  25180  frghash2spot  25184  frgregordn0  25191  frgraregorufrg  25193  frgrareggt1  25237  friendshipgt3  25242
  Copyright terms: Public domain W3C validator