Theorem uvtx2vtx1edg

Description: If a graph has two vertices, and there is an edge between the vertices, then each vertex is universal. (Contributed by AV, 1-Nov-2020) (Revised by AV, 25-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

	Ref	Expression
Hypotheses	uvtxel.v	|- V = ( Vtx ` G )
	isuvtx.e	|- E = ( Edg ` G )
Assertion	uvtx2vtx1edg	|- ( ( ( # ` V ) = 2 /\ V e. E ) -> A. v e. V v e. ( UnivVtx ` G ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	|- V = ( Vtx ` G )
2		isuvtx.e	|- E = ( Edg ` G )
3	1 2	nbgr2vtx1edg	|- ( ( ( # ` V ) = 2 /\ V e. E ) -> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) )
4	1	uvtxel	|- ( v e. ( UnivVtx ` G ) <-> ( v e. V /\ A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
5	4	a1i	|- ( ( ( # ` V ) = 2 /\ V e. E ) -> ( v e. ( UnivVtx ` G ) <-> ( v e. V /\ A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) ) )
6	5	baibd	|- ( ( ( ( # ` V ) = 2 /\ V e. E ) /\ v e. V ) -> ( v e. ( UnivVtx ` G ) <-> A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
7	6	ralbidva	|- ( ( ( # ` V ) = 2 /\ V e. E ) -> ( A. v e. V v e. ( UnivVtx ` G ) <-> A. v e. V A. n e. ( V \ { v } ) n e. ( G NeighbVtx v ) ) )
8	3 7	mpbird	|- ( ( ( # ` V ) = 2 /\ V e. E ) -> A. v e. V v e. ( UnivVtx ` G ) )