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