Theorem isusgrs

Description: The property of being a simple graph, simplified version of isusgr . (Contributed by Alexander van der Vekens, 13-Aug-2017) (Revised by AV, 13-Oct-2020) (Proof shortened by AV, 24-Nov-2020)

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

Proof

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