Theorem isausgr

Description: The property of an unordered pair to be an alternatively defined simple graph, defined as a pair (V,E) of a set V (vertex set) and a set of unordered pairs of elements of V (edge set). (Contributed by Alexander van der Vekens, 28-Aug-2017)

	Ref	Expression
Hypothesis	ausgr.1	|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
Assertion	isausgr	|- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	|- G = { <. v , e >. | e C_ { x e. ~P v | ( # ` x ) = 2 } }
2		simpr	|- ( ( v = V /\ e = E ) -> e = E )
3		pweq	|- ( v = V -> ~P v = ~P V )
4	3	adantr	|- ( ( v = V /\ e = E ) -> ~P v = ~P V )
5	4	rabeqdv	|- ( ( v = V /\ e = E ) -> { x e. ~P v | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
6	2 5	sseq12d	|- ( ( v = V /\ e = E ) -> ( e C_ { x e. ~P v | ( # ` x ) = 2 } <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )
7	6 1	brabga	|- ( ( V e. W /\ E e. X ) -> ( V G E <-> E C_ { x e. ~P V | ( # ` x ) = 2 } ) )