Theorem iswspthn

Description: An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

	Ref	Expression
Assertion	iswspthn	|- ( W e. ( N WSPathsN G ) <-> ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( w = W -> ( f ( SPaths ` G ) w <-> f ( SPaths ` G ) W ) )
2	1	exbidv	|- ( w = W -> ( E. f f ( SPaths ` G ) w <-> E. f f ( SPaths ` G ) W ) )
3		wspthsn	|- ( N WSPathsN G ) = { w e. ( N WWalksN G ) | E. f f ( SPaths ` G ) w }
4	2 3	elrab2	|- ( W e. ( N WSPathsN G ) <-> ( W e. ( N WWalksN G ) /\ E. f f ( SPaths ` G ) W ) )