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 } e. _V

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( Walks ` G ) e. _V
2 opabss 
 |-  { <. f , p >. | f ( Walks ` G ) p } C_ ( Walks ` G )
3 1 2 ssexi 
 |-  { <. f , p >. | f ( Walks ` G ) p } e. _V