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

Theorem usgraedg2 27347
 Description: The value of the "edge function" of a graph is a set containing two elements (the vertices the corresponding edge is connecting), analogous to umgrale 24157. (Contributed by Alexander van der Vekens, 11-Aug-2017.)
Assertion
Ref Expression
usgraedg2 USGrph

Proof of Theorem usgraedg2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 usgraf 27327 . . . 4 USGrph
2 f1f 5475 . . . 4
31, 2syl 15 . . 3 USGrph
43ffvelrnda 5703 . 2 USGrph
5 fveq2 5563 . . . . 5
65eqeq1d 2324 . . . 4
76elrab 2957 . . 3
87simprbi 450 . 2
94, 8syl 15 1 USGrph
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   wceq 1633   wcel 1701  crab 2581   cdif 3183  c0 3489  cpw 3659  csn 3674   class class class wbr 4060   cdm 4726  wf 5288  wf1 5289  cfv 5292  c2 9840  chash 11384   USGrph cusg 27317 This theorem is referenced by:  usgraedgprv  27348  usgranloop  27350 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fv 5300  df-usgra 27319
 Copyright terms: Public domain W3C validator