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

Theorem frgra1v 30725
 Description: Any graph with only one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
Assertion
Ref Expression
frgra1v USGrph FriendGrph

Proof of Theorem frgra1v
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgrav 23402 . . 3 USGrph
2 simplr 754 . . . . 5 USGrph USGrph
3 ral0 3879 . . . . . 6
4 sneq 3982 . . . . . . . . . . 11
54difeq2d 3569 . . . . . . . . . 10
6 difid 3842 . . . . . . . . . 10
75, 6syl6eq 2507 . . . . . . . . 9
8 preq2 4050 . . . . . . . . . . . 12
98preq1d 4055 . . . . . . . . . . 11
109sseq1d 3478 . . . . . . . . . 10
1110reubidv 2998 . . . . . . . . 9
127, 11raleqbidv 3024 . . . . . . . 8
1312ralsng 4007 . . . . . . 7
1413adantl 466 . . . . . 6 USGrph
153, 14mpbiri 233 . . . . 5 USGrph
16 isfrgra 30717 . . . . . 6 FriendGrph USGrph
1716ad2antrr 725 . . . . 5 USGrph FriendGrph USGrph
182, 15, 17mpbir2and 913 . . . 4 USGrph FriendGrph
1918ex 434 . . 3 USGrph FriendGrph
201, 19mpancom 669 . 2 USGrph FriendGrph
2120impcom 430 1 USGrph FriendGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758  wral 2793  wreu 2795  cvv 3065   cdif 3420   wss 3423  c0 3732  csn 3972  cpr 3974   class class class wbr 4387   crn 4936   USGrph cusg 23396   FriendGrph cfrgra 30715 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 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4508  ax-nul 4516  ax-pr 4626 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 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2599  df-ne 2644  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3067  df-sbc 3282  df-dif 3426  df-un 3428  df-in 3430  df-ss 3437  df-nul 3733  df-if 3887  df-sn 3973  df-pr 3975  df-op 3979  df-br 4388  df-opab 4446  df-xp 4941  df-rel 4942  df-cnv 4943  df-dm 4945  df-rn 4946  df-usgra 23398  df-frgra 30716 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator