Theorem isumgrs

Description: The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

	Ref	Expression
Hypotheses	isumgr.v	|- V = ( Vtx ` G )
	isumgr.e	|- E = ( iEdg ` G )
Assertion	isumgrs	|- ( G e. U -> ( G e. UMGraph <-> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		isumgr.v	|- V = ( Vtx ` G )
2		isumgr.e	|- E = ( iEdg ` G )
3	1 2	isumgr	|- ( G e. U -> ( G e. UMGraph <-> E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } ) )
4		prprrab	|- { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 }
5	4	a1i	|- ( G e. U -> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } = { x e. ~P V | ( # ` x ) = 2 } )
6	5	feq3d	|- ( G e. U -> ( E : dom E --> { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 } <-> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } ) )
7	3 6	bitrd	|- ( G e. U -> ( G e. UMGraph <-> E : dom E --> { x e. ~P V | ( # ` x ) = 2 } ) )