Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frisusgra Structured version   Unicode version

Theorem frisusgra 30708
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 30707 . 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 459 1  |-  ( V FriendGrph  E  ->  V USGrph  E )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wral 2792   E!wreu 2794    \ cdif 3409    C_ wss 3412   {csn 3961   {cpr 3963   class class class wbr 4376   ran crn 4925   USGrph cusg 23385   FriendGrph cfrgra 30704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429  ax-sep 4497  ax-nul 4505  ax-pr 4615
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-eu 2263  df-mo 2264  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-ne 2643  df-ral 2797  df-rex 2798  df-reu 2799  df-rab 2801  df-v 3056  df-dif 3415  df-un 3417  df-in 3419  df-ss 3426  df-nul 3722  df-if 3876  df-sn 3962  df-pr 3964  df-op 3968  df-br 4377  df-opab 4435  df-xp 4930  df-rel 4931  df-cnv 4932  df-dm 4934  df-rn 4935  df-frgra 30705
This theorem is referenced by:  frgra0v  30709  frgra2v  30715  3vfriswmgra  30721  2pthfrgrarn2  30726  2pthfrgra  30727  3cyclfrgrarn  30729  3cyclfrgrarn2  30730  3cyclfrgra  30731  n4cyclfrgra  30734  frgranbnb  30736  frconngra  30737  vdfrgra0  30738  vdgfrgra0  30739  vdn0frgrav2  30740  vdgn0frgrav2  30741  vdn1frgrav2  30742  vdgn1frgrav2  30743  vdgfrgragt2  30744  frgrancvvdeqlem2  30748  frgrancvvdeqlem3  30749  frgrancvvdeqlem4  30750  frgrancvvdeqlem7  30753  frgrancvvdeqlemC  30756  frgrancvvdeq  30759  frgrancvvdgeq  30760  frgrawopreglem1  30761  frgrawopreglem2  30762  frgrawopreglem4  30764  frgrawopreg  30766  frgraeu  30771  frg2woteu  30772  frg2wot1  30774  frg2spot1  30775  frg2woteqm  30776  frghash2spot  30780  frgregordn0  30787  frgraregorufrg  30789  frgrareggt1  30833  friendshipgt3  30838
  Copyright terms: Public domain W3C validator