Metamath Proof Explorer

Theorem wlkRes

Description: Restrictions of walks (i.e. special kinds of walks, for example paths - see pthsfval ) are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 30-Dec-2020) (Proof shortened by AV, 15-Jan-2021)

Ref Expression
Hypothesis wlkRes.1 ⊢ f W ⁡ G p → f Walks ⁡ G p
Assertion wlkRes ⊢ f p | f W ⁡ G p ∧ φ ∈ V

Proof

Step Hyp Ref Expression
1 wlkRes.1 ⊢ f W ⁡ G p → f Walks ⁡ G p
2 1 gen2 ⊢ ∀ f ∀ p f W ⁡ G p → f Walks ⁡ G p
3 wksv ⊢ f p | f Walks ⁡ G p ∈ V
4 opabbrex ⊢ ∀ f ∀ p f W ⁡ G p → f Walks ⁡ G p ∧ f p | f Walks ⁡ G p ∈ V → f p | f W ⁡ G p ∧ φ ∈ V
5 2 3 4 mp2an ⊢ f p | f W ⁡ G p ∧ φ ∈ V