Metamath Proof Explorer

Theorem wlkResOLD

Description: Obsolete version of opabresex2 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 30-Dec-2020) (Proof shortened by AV, 15-Jan-2021) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 wlkResOLD.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