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

Theorem isuslgra 28113
 Description: The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)
Assertion
Ref Expression
isuslgra USLGrph
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem isuslgra
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1eq1 5434 . . . 4
3 dmeq 4881 . . . . 5
43adantl 452 . . . 4
5 f1eq2 5435 . . . 4
64, 5syl 15 . . 3
7 simpl 443 . . . . . 6
87pweqd 3632 . . . . 5
98difeq1d 3295 . . . 4
10 rabeq 2784 . . . 4
11 f1eq3 5436 . . . 4
129, 10, 113syl 18 . . 3
132, 6, 123bitrd 270 . 2
14 df-uslgra 28107 . 2 USLGrph
1513, 14brabga 4281 1 USLGrph
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1625   wcel 1686  crab 2549   cdif 3151  c0 3457  cpw 3627  csn 3642   class class class wbr 4025   cdm 4691  wf1 5254  cfv 5257   cle 8870  c2 9797  chash 11339   USLGrph cuslg 28105 This theorem is referenced by:  uslgraf  28115  uslisumgra  28123  usisuslgra  28124  uslgra1  28129 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-uslgra 28107
 Copyright terms: Public domain W3C validator