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

Metamath Proof Explorer

Theorem wksv

Description: The class of walks is a set. (Contributed by AV, 15-Jan-2021) (Proof shortened by SN, 11-Dec-2024)

		Ref	Expression
	Assertion	wksv	$⊢ \{⟨f, p⟩ \| f Walks (G) p\} \in V$

Step	Hyp	Ref	Expression
1		fvex	$⊢ Walks (G) \in V$
2		opabss	$⊢ \{⟨f, p⟩ \| f Walks (G) p\} \subseteq Walks (G)$
3	1 2	ssexi	$⊢ \{⟨f, p⟩ \| f Walks (G) p\} \in V$