This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isausgr

Description: The property of an ordered 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 } ) )