Theorem isfusgr

Description: The property of being a finite simple graph. (Contributed by AV, 3-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypothesis	isfusgr.v	|- V = ( Vtx ` G )
Assertion	isfusgr	|- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isfusgr.v	|- V = ( Vtx ` G )
2		fveq2	|- ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
3	2 1	eqtr4di	|- ( g = G -> ( Vtx ` g ) = V )
4	3	eleq1d	|- ( g = G -> ( ( Vtx ` g ) e. Fin <-> V e. Fin ) )
5		df-fusgr	|- FinUSGraph = { g e. USGraph | ( Vtx ` g ) e. Fin }
6	4 5	elrab2	|- ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )