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

Theorem isfrgra 30720
 Description: The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.)
Assertion
Ref Expression
isfrgra FriendGrph USGrph
Distinct variable groups:   ,,,   ,,,
Allowed substitution hints:   (,,)   (,,)

Proof of Theorem isfrgra
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq1 4393 . . 3 USGrph USGrph
2 difeq1 3565 . . . . 5
3 reueq1 3015 . . . . 5
42, 3raleqbidv 3027 . . . 4
54raleqbi1dv 3021 . . 3
61, 5anbi12d 710 . 2 USGrph USGrph
7 breq2 4394 . . 3 USGrph USGrph
8 rneq 5163 . . . . . 6
98sseq2d 3482 . . . . 5
109reubidv 3001 . . . 4
11102ralbidv 2861 . . 3
127, 11anbi12d 710 . 2 USGrph USGrph
13 df-frgra 30719 . 2 FriendGrph USGrph
146, 12, 13brabg 4706 1 FriendGrph USGrph
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1370   wcel 1758  wral 2795  wreu 2797   cdif 3423   wss 3426  csn 3975  cpr 3977   class class class wbr 4390   crn 4939   USGrph cusg 23399   FriendGrph cfrgra 30718 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 4511  ax-nul 4519  ax-pr 4629 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 2601  df-ne 2646  df-ral 2800  df-reu 2802  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391  df-opab 4449  df-cnv 4946  df-dm 4948  df-rn 4949  df-frgra 30719 This theorem is referenced by:  frisusgrapr  30721  frgra0v  30723  frgra1v  30728  frgra2v  30729  frgra3v  30732
 Copyright terms: Public domain W3C validator