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

Theorem nbgrel 39410
 Description: Characterization of a neighbor of a vertex in a graph . (Contributed by Alexander van der Vekens and Mario Carneiro, 9-Oct-2017.) (Revised by AV, 26-Oct-2020.)
Hypotheses
Ref Expression
nbgrel.v Vtx
nbgrel.e Edg
Assertion
Ref Expression
nbgrel NeighbVtx
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem nbgrel
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nbgr 39401 . . . . . 6 NeighbVtx Vtx Vtx Edg
21mpt2xeldm 6957 . . . . 5 NeighbVtx Vtx
3 csbfv 5902 . . . . . . . . 9 Vtx Vtx
4 nbgrel.v . . . . . . . . 9 Vtx
53, 4eqtr4i 2476 . . . . . . . 8 Vtx
65eleq2i 2521 . . . . . . 7 Vtx
76biimpi 198 . . . . . 6 Vtx
87adantl 468 . . . . 5 Vtx
92, 8syl 17 . . . 4 NeighbVtx
109a1i 11 . . 3 NeighbVtx
1110pm4.71rd 641 . 2 NeighbVtx NeighbVtx
12 nbgrel.e . . . . . . 7 Edg
134, 12nbgrval 39406 . . . . . 6 NeighbVtx
1413eleq2d 2514 . . . . 5 NeighbVtx
15 preq2 4052 . . . . . . . . 9
1615sseq1d 3459 . . . . . . . 8
1716rexbidv 2901 . . . . . . 7
1817elrab 3196 . . . . . 6
19 eldifsn 4097 . . . . . . 7
2019anbi1i 701 . . . . . 6
21 anass 655 . . . . . 6
2218, 20, 213bitri 275 . . . . 5
2314, 22syl6bb 265 . . . 4 NeighbVtx
2423pm5.32da 647 . . 3 NeighbVtx
25 3anass 989 . . . 4
26 ancom 452 . . . . 5
2726anbi1i 701 . . . 4
28 anass 655 . . . 4
2925, 27, 283bitrri 276 . . 3
3024, 29syl6bb 265 . 2 NeighbVtx
3111, 30bitrd 257 1 NeighbVtx
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   w3a 985   wceq 1444   wcel 1887   wne 2622  wrex 2738  crab 2741  cvv 3045  csb 3363   cdif 3401   wss 3404  csn 3968  cpr 3970  cfv 5582  (class class class)co 6290  Vtxcvtx 39101  Edgcedga 39210   NeighbVtx cnbgr 39397 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-nbgr 39401 This theorem is referenced by:  nbgr2vtx1edg  39418  nbuhgr2vtx1edgblem  39419  nbuhgr2vtx1edgb  39420  nbgrisvtx  39427  nbgrsym  39437  isuvtxa  39467  iscplgredg  39485  cusgrexi  39507
 Copyright terms: Public domain W3C validator